vstd/resource/impls/
frac_opt.rs

1use super::super::super::modes::*;
2use super::super::super::prelude::*;
3use super::super::Loc;
4use super::super::storage_protocol::*;
5
6verus! {
7
8broadcast use {
9    super::super::super::imap::group_imap_lemmas,
10    super::super::super::iset::group_iset_lemmas,
11    super::super::super::map::group_map_lemmas,
12    super::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    /// Allowed values for a token's quantity when there is another token.
249    pub proof fn bounded_with(tracked &mut self, tracked other: &Self)
250        requires
251            self.id() == other.id(),
252        ensures
253            0.0real < (old(self).frac() + other.frac()) <= 1.0real,
254            *old(self) == *final(self),
255    {
256        use_type_invariant(&*self);
257        use_type_invariant(other);
258        self.r.validate_with_shared(&other.r);
259    }
260
261    /// Obtain shared access to the underlying resource.
262    pub proof fn borrow(tracked &self) -> (tracked ret: &T)
263        ensures
264            ret == self.resource(),
265    {
266        use_type_invariant(self);
267        StorageResource::guard(&self.r, imap![() => self.resource()]).tracked_borrow(())
268    }
269
270    /// Reclaim full ownership of the underlying resource.
271    pub proof fn take_resource(tracked self) -> (tracked pair: (T, Empty<T>))
272        requires
273            self.frac() == 1 as real,
274        ensures
275            pair.0 == self.resource(),
276            pair.1.id() == self.id(),
277    {
278        use_type_invariant(&self);
279        self.r.validate();
280
281        let p1 = self.r.value();
282        let p2 = FractionalCarrierOpt::Value { v: None, frac: (1 as real) };
283        let b2 = imap![() => self.resource()];
284        assert forall|q: FractionalCarrierOpt<T>, t1: IMap<(), T>|
285            #![all_triggers]
286            FractionalCarrierOpt::rel(FractionalCarrierOpt::op(p1, q), t1) implies exists|
287            t2: IMap<(), T>,
288        |
289            #![all_triggers]
290            FractionalCarrierOpt::rel(FractionalCarrierOpt::op(p2, q), t2) && t2.dom().disjoint(
291                b2.dom(),
292            ) && t1 =~= t2.union_prefer_right(b2) by {
293            let t2 = imap![];
294            assert(FractionalCarrierOpt::rel(FractionalCarrierOpt::op(p2, q), t2));
295            assert(t2.dom().disjoint(b2.dom()));
296            assert(t1 =~= t2.union_prefer_right(b2));
297        }
298
299        let tracked Self { r } = self;
300        let tracked (new_r, mut m) = r.withdraw(p2, b2);
301        let tracked emp = Empty { r: new_r };
302        let tracked resource = m.tracked_remove(());
303        (resource, emp)
304    }
305}
306
307impl<T> Empty<T> {
308    #[verifier::type_invariant]
309    spec fn inv(self) -> bool {
310        &&& self.r.value() matches FractionalCarrierOpt::Value { v: None, frac }
311        &&& frac == 1 as real
312    }
313
314    pub closed spec fn id(self) -> Loc {
315        self.r.loc()
316    }
317
318    pub proof fn new(tracked v: T) -> (tracked result: Self) {
319        let f = FractionalCarrierOpt::<T>::Value { v: None, frac: (1 as real) };
320        let tracked mut m = IMap::<(), T>::tracked_empty();
321        let tracked r = StorageResource::alloc(f, m);
322        Self { r }
323    }
324
325    /// Give up ownership of a resource and obtain a [`Frac`] token.
326    pub proof fn put_resource(tracked self, tracked resource: T) -> (tracked frac: Frac<T>)
327        ensures
328            frac.id() == self.id(),
329            frac.resource() == resource,
330            frac.frac() == 1 as real,
331    {
332        use_type_invariant(&self);
333        self.r.validate();
334
335        let p1 = self.r.value();
336        let b1 = imap![() => resource];
337        let p2 = FractionalCarrierOpt::Value { v: Some(resource), frac: (1 as real) };
338
339        assert forall|q: FractionalCarrierOpt<T>, t1: IMap<(), T>|
340            #![all_triggers]
341            FractionalCarrierOpt::rel(FractionalCarrierOpt::op(p1, q), t1) implies exists|
342            t2: IMap<(), T>,
343        |
344            #![all_triggers]
345            FractionalCarrierOpt::rel(FractionalCarrierOpt::op(p2, q), t2) && t1.dom().disjoint(
346                b1.dom(),
347            ) && t1.union_prefer_right(b1) =~= t2 by {
348            let t2 = imap![() => resource];
349            assert(FractionalCarrierOpt::rel(FractionalCarrierOpt::op(p2, q), t2)
350                && t1.dom().disjoint(b1.dom()) && t1.union_prefer_right(b1) =~= t2);
351        }
352
353        let tracked mut m = IMap::tracked_empty();
354        m.tracked_insert((), resource);
355        let tracked Self { r } = self;
356        let tracked new_r = r.deposit(m, p2);
357        let tracked f = Frac { r: new_r };
358        f
359    }
360}
361
362} // verus!
vstd/resource/impls/frac_opt.rs

vstd/resource/impls/
frac_opt.rs
