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

vstd/resource/
frac_opt.rs
