vstd/resource/
frac_opt.rs

1use super::super::modes::*;
2use super::super::prelude::*;
3use super::Loc;
4use super::storage_protocol::*;
5
6verus! {
7
8broadcast use {
9    super::super::imap::group_imap_lemmas,
10    super::super::iset::group_iset_lemmas,
11    super::super::map::group_map_lemmas,
12    super::super::set::group_set_lemmas,
13};
14
15/////// Fractional tokens that allow borrowing of resources
16enum FractionalCarrierOpt<T> {
17    Value { v: Option<T>, frac: real },
18    Empty,
19    Invalid,
20}
21
22impl<T> Protocol<(), T> for FractionalCarrierOpt<T> {
23    closed spec fn op(self, other: Self) -> Self {
24        match self {
25            FractionalCarrierOpt::Invalid => FractionalCarrierOpt::Invalid,
26            FractionalCarrierOpt::Empty => other,
27            FractionalCarrierOpt::Value { v: sv, frac: s_frac } => match other {
28                FractionalCarrierOpt::Invalid => FractionalCarrierOpt::Invalid,
29                FractionalCarrierOpt::Empty => self,
30                FractionalCarrierOpt::Value { v: ov, frac: o_frac } => {
31                    if sv != ov {
32                        FractionalCarrierOpt::Invalid
33                    } else if s_frac <= (0 as real) || o_frac <= (0 as real) || s_frac + o_frac > (
34                    1 as real) {
35                        FractionalCarrierOpt::Invalid
36                    } else {
37                        FractionalCarrierOpt::Value { v: sv, frac: s_frac + o_frac }
38                    }
39                },
40            },
41        }
42    }
43
44    closed spec fn rel(self, s: IMap<(), T>) -> bool {
45        match self {
46            FractionalCarrierOpt::Value { v, frac } => {
47                (match v {
48                    Some(v0) => s.dom().contains(()) && s[()] == v0,
49                    None => s =~= imap![],
50                }) && frac == 1 as real
51            },
52            FractionalCarrierOpt::Empty => false,
53            FractionalCarrierOpt::Invalid => false,
54        }
55    }
56
57    closed spec fn unit() -> Self {
58        FractionalCarrierOpt::Empty
59    }
60
61    proof fn commutative(a: Self, b: Self) {
62    }
63
64    proof fn associative(a: Self, b: Self, c: Self) {
65    }
66
67    proof fn op_unit(a: Self) {
68    }
69}
70
71/// Token that maintains fractional access to some resource.
72/// This allows multiple clients to obtain shared references to some resource
73/// via `borrow`.
74pub tracked struct Frac<T> {
75    r: StorageResource<(), T, FractionalCarrierOpt<T>>,
76}
77
78/// Token that represents the "empty" state of a fractional resource system.
79/// See [`Frac`] for more information.
80pub tracked struct Empty<T> {
81    r: StorageResource<(), T, FractionalCarrierOpt<T>>,
82}
83
84impl<T> Frac<T> {
85    #[verifier::type_invariant]
86    spec fn inv(self) -> bool {
87        self.r.value() matches FractionalCarrierOpt::Value { v: Some(_), .. }
88    }
89
90    pub closed spec fn id(self) -> Loc {
91        self.r.loc()
92    }
93
94    pub closed spec fn resource(self) -> T {
95        self.r.value()->v.unwrap()
96    }
97
98    pub closed spec fn frac(self) -> real {
99        self.r.value()->frac
100    }
101
102    pub open spec fn valid(self, id: Loc, frac: real) -> bool {
103        &&& self.id() == id
104        &&& self.frac() == frac
105    }
106
107    /// Create a fractional token that maintains shared access to the input resource.
108    pub proof fn new(tracked v: T) -> (tracked result: Self)
109        ensures
110            result.frac() == 1 as real,
111            result.resource() == v,
112    {
113        let f = FractionalCarrierOpt::<T>::Value { v: Some(v), frac: (1 as real) };
114        let tracked mut m = IMap::<(), T>::tracked_empty();
115        m.tracked_insert((), v);
116        let tracked r = StorageResource::alloc(f, m);
117        Self { r }
118    }
119
120    /// Two tokens agree on values of the underlying resource.
121    pub proof fn agree(tracked self: &Self, tracked other: &Self)
122        requires
123            self.id() == other.id(),
124        ensures
125            self.resource() == other.resource(),
126    {
127        use_type_invariant(self);
128        use_type_invariant(other);
129        let tracked joined = self.r.join_shared(&other.r);
130        joined.validate();
131    }
132
133    // This helper is needed to bypass the type invariant temporarily
134    proof fn split_to_helper(
135        tracked r: &mut StorageResource<(), T, FractionalCarrierOpt<T>>,
136        frac: real,
137    ) -> (tracked result: Self)
138        requires
139            (0 as real) < frac < old(r).value()->frac,
140            old(r).value() matches FractionalCarrierOpt::Value { v: Some(_), .. },
141        ensures
142            final(r).loc() == old(r).loc(),
143            result.id() == old(r).loc(),
144            final(r).value()->v.unwrap() == old(r).value()->v.unwrap(),
145            result.resource() == old(r).value()->v.unwrap(),
146            final(r).value()->frac + result.frac() == old(r).value()->frac,
147            result.frac() == frac,
148            final(r).value() matches FractionalCarrierOpt::Value { v: Some(_), .. },
149    {
150        r.validate();
151        let tracked mut r1 = StorageResource::alloc(
152            FractionalCarrierOpt::Value { v: None, frac: (1 as real) },
153            IMap::tracked_empty(),
154        );
155        tracked_swap(r, &mut r1);
156        let tracked (r1, r2) = r1.split(
157            FractionalCarrierOpt::Value { v: r1.value()->v, frac: r1.value()->frac - frac },
158            FractionalCarrierOpt::Value { v: r1.value()->v, frac: frac },
159        );
160        *r = r1;
161        Self { r: r2 }
162    }
163
164    /// Split one resource into two resources whose quantities sum to the original.
165    /// The returned token has quantity `result_frac`; the new value of the input token has
166    /// quantity `old(self).frac() - result_frac`.
167    pub proof fn split_to(tracked &mut self, result_frac: real) -> (tracked result: Self)
168        requires
169            (0 as real) < result_frac < old(self).frac(),
170        ensures
171            final(self).id() == old(self).id(),
172            result.id() == old(self).id(),
173            final(self).resource() == old(self).resource(),
174            result.resource() == old(self).resource(),
175            final(self).frac() == old(self).frac() - result_frac,
176            result.frac() == result_frac,
177    {
178        use_type_invariant(&*self);
179        Self::split_to_helper(&mut self.r, result_frac)
180    }
181
182    /// Split one resource by half into two resources whose quantities sum to the original.
183    /// The returned token has quantity `n`; the new value of the input token has
184    /// quantity `old(self).frac() - n`.
185    pub proof fn split(tracked &mut self) -> (tracked result: Self)
186        ensures
187            final(self).id() == old(self).id(),
188            result.id() == old(self).id(),
189            final(self).resource() == old(self).resource(),
190            result.resource() == old(self).resource(),
191            final(self).frac() == old(self).frac() / 2 as real,
192            result.frac() == old(self).frac() / 2 as real,
193    {
194        use_type_invariant(&*self);
195        self.r.validate();
196        self.split_to(self.frac() / 2 as real)
197    }
198
199    /// Combine two tokens, summing their quantities.
200    pub proof fn combine(tracked &mut self, tracked other: Self)
201        requires
202            old(self).id() == other.id(),
203        ensures
204            final(self).id() == old(self).id(),
205            final(self).resource() == old(self).resource(),
206            final(self).resource() == other.resource(),
207            final(self).frac() == old(self).frac() + other.frac(),
208    {
209        use_type_invariant(&*self);
210        Self::combine_helper(&mut self.r, other);
211    }
212
213    // This helper is needed to temporarily bypass the type invariant
214    proof fn combine_helper(
215        tracked r: &mut StorageResource<(), T, FractionalCarrierOpt<T>>,
216        tracked other: Self,
217    )
218        requires
219            old(r).loc() == other.id(),
220            old(r).value() matches FractionalCarrierOpt::Value { v: Some(_), .. },
221        ensures
222            final(r).loc() == old(r).loc(),
223            final(r).value()->v.unwrap() == old(r).value()->v.unwrap(),
224            final(r).value()->v.unwrap() == other.resource(),
225            final(r).value()->frac == old(r).value()->frac + other.frac(),
226            final(r).value() matches FractionalCarrierOpt::Value { v: Some(_), .. },
227    {
228        use_type_invariant(&other);
229        r.validate();
230        let tracked mut r1 = StorageResource::alloc(
231            FractionalCarrierOpt::Value { v: None, frac: (1 as real) },
232            IMap::tracked_empty(),
233        );
234        tracked_swap(r, &mut r1);
235        r1.validate_with_shared(&other.r);
236        *r = StorageResource::join(r1, other.r);
237    }
238
239    /// Allowed values for a token's quantity.
240    pub proof fn bounded(tracked &self)
241        ensures
242            (0 as real) < self.frac() <= (1 as real),
243    {
244        use_type_invariant(self);
245        let (x, _) = self.r.validate();
246    }
247
248    /// Obtain shared access to the underlying resource.
249    pub proof fn borrow(tracked &self) -> (tracked ret: &T)
250        ensures
251            ret == self.resource(),
252    {
253        use_type_invariant(self);
254        StorageResource::guard(&self.r, imap![() => self.resource()]).tracked_borrow(())
255    }
256
257    /// Reclaim full ownership of the underlying resource.
258    pub proof fn take_resource(tracked self) -> (tracked pair: (T, Empty<T>))
259        requires
260            self.frac() == 1 as real,
261        ensures
262            pair.0 == self.resource(),
263            pair.1.id() == self.id(),
264    {
265        use_type_invariant(&self);
266        self.r.validate();
267
268        let p1 = self.r.value();
269        let p2 = FractionalCarrierOpt::Value { v: None, frac: (1 as real) };
270        let b2 = imap![() => self.resource()];
271        assert forall|q: FractionalCarrierOpt<T>, t1: IMap<(), T>|
272            #![all_triggers]
273            FractionalCarrierOpt::rel(FractionalCarrierOpt::op(p1, q), t1) implies exists|
274            t2: IMap<(), T>,
275        |
276            #![all_triggers]
277            FractionalCarrierOpt::rel(FractionalCarrierOpt::op(p2, q), t2) && t2.dom().disjoint(
278                b2.dom(),
279            ) && t1 =~= t2.union_prefer_right(b2) by {
280            let t2 = imap![];
281            assert(FractionalCarrierOpt::rel(FractionalCarrierOpt::op(p2, q), t2));
282            assert(t2.dom().disjoint(b2.dom()));
283            assert(t1 =~= t2.union_prefer_right(b2));
284        }
285
286        let tracked Self { r } = self;
287        let tracked (new_r, mut m) = r.withdraw(p2, b2);
288        let tracked emp = Empty { r: new_r };
289        let tracked resource = m.tracked_remove(());
290        (resource, emp)
291    }
292}
293
294impl<T> Empty<T> {
295    #[verifier::type_invariant]
296    spec fn inv(self) -> bool {
297        &&& self.r.value() matches FractionalCarrierOpt::Value { v: None, frac }
298        &&& frac == 1 as real
299    }
300
301    pub closed spec fn id(self) -> Loc {
302        self.r.loc()
303    }
304
305    pub proof fn new(tracked v: T) -> (tracked result: Self) {
306        let f = FractionalCarrierOpt::<T>::Value { v: None, frac: (1 as real) };
307        let tracked mut m = IMap::<(), T>::tracked_empty();
308        let tracked r = StorageResource::alloc(f, m);
309        Self { r }
310    }
311
312    /// Give up ownership of a resource and obtain a [`Frac`] token.
313    pub proof fn put_resource(tracked self, tracked resource: T) -> (tracked frac: Frac<T>)
314        ensures
315            frac.id() == self.id(),
316            frac.resource() == resource,
317            frac.frac() == 1 as real,
318    {
319        use_type_invariant(&self);
320        self.r.validate();
321
322        let p1 = self.r.value();
323        let b1 = imap![() => resource];
324        let p2 = FractionalCarrierOpt::Value { v: Some(resource), frac: (1 as real) };
325
326        assert forall|q: FractionalCarrierOpt<T>, t1: IMap<(), T>|
327            #![all_triggers]
328            FractionalCarrierOpt::rel(FractionalCarrierOpt::op(p1, q), t1) implies exists|
329            t2: IMap<(), T>,
330        |
331            #![all_triggers]
332            FractionalCarrierOpt::rel(FractionalCarrierOpt::op(p2, q), t2) && t1.dom().disjoint(
333                b1.dom(),
334            ) && t1.union_prefer_right(b1) =~= t2 by {
335            let t2 = imap![() => resource];
336            assert(FractionalCarrierOpt::rel(FractionalCarrierOpt::op(p2, q), t2)
337                && t1.dom().disjoint(b1.dom()) && t1.union_prefer_right(b1) =~= t2);
338        }
339
340        let tracked mut m = IMap::tracked_empty();
341        m.tracked_insert((), resource);
342        let tracked Self { r } = self;
343        let tracked new_r = r.deposit(m, p2);
344        let tracked f = Frac { r: new_r };
345        f
346    }
347}
348
349} // verus!
vstd/resource/frac_opt.rs

vstd/resource/
frac_opt.rs
