vstd/resource/
frac.rs

1use super::super::modes::*;
2use super::super::prelude::*;
3use super::Loc;
4use super::agree::AgreementRA;
5use super::algebra::Resource;
6use super::algebra::ResourceAlgebra;
7use super::pcm::PCM;
8use super::product::ProductRA;
9use super::storage_protocol::*;
10use super::*;
11
12verus! {
13
14broadcast use {super::super::map::group_map_axioms, super::super::set::group_set_axioms};
15
16pub enum FractionRA {
17    Frac(real),
18    Invalid,
19}
20
21impl FractionRA {
22    pub open spec fn new(f: real) -> Self
23        recommends
24            0real < f <= 1real,
25    {
26        FractionRA::Frac(f)
27    }
28
29    pub open spec fn frac(self) -> real
30        recommends
31            self is Frac,
32    {
33        self->Frac_0
34    }
35}
36
37impl ResourceAlgebra for FractionRA {
38    open spec fn valid(self) -> bool {
39        match self {
40            FractionRA::Invalid => false,
41            FractionRA::Frac(frac) => (0 as real) < frac <= (1 as real),
42        }
43    }
44
45    open spec fn op(a: Self, b: Self) -> Self {
46        match (a, b) {
47            (FractionRA::Invalid, _) => FractionRA::Invalid,
48            (_, FractionRA::Invalid) => FractionRA::Invalid,
49            (FractionRA::Frac(a_frac), FractionRA::Frac(b_frac)) => {
50                if !a.valid() || !b.valid() {
51                    FractionRA::Invalid
52                } else if a_frac + b_frac <= (1 as real) {
53                    FractionRA::Frac(a_frac + b_frac)
54                } else {
55                    FractionRA::Invalid
56                }
57            },
58        }
59    }
60
61    proof fn valid_op(a: Self, b: Self) {
62    }
63
64    proof fn commutative(a: Self, b: Self) {
65    }
66
67    proof fn associative(a: Self, b: Self, c: Self) {
68    }
69}
70
71pub proof fn lemma_whole_fraction_has_no_frame(a: FractionRA)
72    requires
73        a == FractionRA::Frac(1 as real),
74    ensures
75        forall|b: FractionRA|
76            #![trigger FractionRA::op(a, b).valid()]
77            !FractionRA::op(a, b).valid(),
78{
79    assert forall|b: FractionRA|
80        #![trigger FractionRA::op(a, b).valid()]
81        !FractionRA::op(a, b).valid() by {
82        if FractionRA::op(a, b).valid() {
83            FractionRA::commutative(a, b);
84            FractionRA::valid_op(b, a);
85            assert(b.valid());
86            assert(b is Frac);
87            assert((0 as real) < b->Frac_0 <= (1 as real));
88            assert(a->Frac_0 + b->Frac_0 > (1 as real));  // CONTRADICTION
89        };
90    }
91}
92
93type FractionalCarrier<T> = ProductRA<FractionRA, AgreementRA<T>>;
94
95/// An implementation of a resource for fractional ownership of a ghost variable.
96///
97/// If you just want to split the permission in half, you can also use the
98/// [`GhostVar<T>`](super::ghost_var::GhostVar) and [`GhostVarAuth<T>`](super::ghost_var::GhostVarAuth) library.
99///
100/// ### Example
101///
102/// ```
103/// fn example_use() {
104///     let tracked mut r = FracGhost::<u64>::new(123);
105///     assert(r@ == 123);
106///     assert(r.frac() == 1 as real);
107///     let tracked r2 = r.split();
108///     assert(r@ == 123);
109///     assert(r2@ == 123);
110///     assert(r.frac() == (0.5 as real));
111///     assert(r2.frac() == (0.5 as real));
112///     proof {
113///         r.combine(r2);
114///         r.update(456);
115///     }
116///     assert(r@ == 456);
117///     assert(r.frac() == 3 as real);
118///
119///     let tracked mut a = FracGhost::<u32>::new(5);
120///     assert(a@ == 5);
121///     assert(a.frac() == 1real);
122///     let tracked mut b = a.split();
123///     assert(a.frac() == (0.5 as real));
124///     assert(b.frac() == (0.5 as real));
125///     proof {
126///         a.update_with(&mut b, 123);
127///     }
128///     assert(a@ == 123);
129///
130///     proof {
131///         a.combine(b);
132///         a.update(6);
133///     }
134///     assert(a@ == 6);
135/// }
136/// ```
137pub tracked struct FracGhost<T> {
138    r: Resource<FractionalCarrier<T>>,
139}
140
141impl<T> FracGhost<T> {
142    #[verifier::type_invariant]
143    spec fn inv(self) -> bool {
144        &&& self.r.value().left is Frac
145        &&& self.r.value().right is Agree
146    }
147
148    pub closed spec fn id(self) -> Loc {
149        self.r.loc()
150    }
151
152    pub closed spec fn view(self) -> T {
153        self.r.value().right->Agree_0
154    }
155
156    /// The fractional quantity of this permission
157    pub closed spec fn frac(self) -> real {
158        self.r.value().left->Frac_0
159    }
160
161    pub open spec fn valid(self, id: Loc, frac: real) -> bool {
162        &&& self.id() == id
163        &&& self.frac() == frac
164    }
165
166    /// Allocate a new resource with the given value.
167    pub proof fn new(v: T) -> (tracked result: Self)
168        ensures
169            result.frac() == 1 as real,
170            result@ == v,
171    {
172        let f = FractionalCarrier {
173            left: FractionRA::Frac(1 as real),
174            right: AgreementRA::Agree(v),
175        };
176        let tracked r = Resource::alloc(f);
177        Self { r }
178    }
179
180    /// Two resources agree on their values.
181    pub proof fn agree(tracked self: &Self, tracked other: &Self)
182        requires
183            self.id() == other.id(),
184        ensures
185            self@ == other@,
186    {
187        use_type_invariant(self);
188        use_type_invariant(other);
189        let tracked joined = self.r.join_shared(&other.r);
190        joined.validate()
191    }
192
193    /// Take a token out of a mutable reference, leaving a meaningless token behind.
194    pub proof fn take(tracked &mut self) -> (tracked result: Self)
195        ensures
196            result == *old(self),
197    {
198        self.bounded();
199        let tracked mut mself = Self::dummy();
200        tracked_swap(self, &mut mself);
201        mself
202    }
203
204    /// Split one resource into two. Both the returned resource and self have half of the original
205    /// fraction.
206    pub proof fn split_to(tracked &mut self, result_frac: real) -> (tracked result: Self)
207        requires
208            (0 as real) < result_frac < old(self).frac(),
209        ensures
210            final(self).id() == old(self).id(),
211            result.id() == final(self).id(),
212            final(self)@ == old(self)@,
213            result@ == old(self)@,
214            final(self).frac() == old(self).frac() - result_frac,
215            result.frac() == result_frac,
216    {
217        self.bounded();
218        let self_frac = self.frac();
219        let tracked mut mself = Self::dummy();
220        tracked_swap(self, &mut mself);
221        use_type_invariant(&mself);
222        let tracked (r1, r2) = mself.r.split(
223            FractionalCarrier {
224                left: FractionRA::Frac(self_frac - result_frac),
225                right: AgreementRA::Agree(mself@),
226            },
227            FractionalCarrier {
228                left: FractionRA::Frac(result_frac),
229                right: AgreementRA::Agree(mself@),
230            },
231        );
232        self.r = r1;
233        Self { r: r2 }
234    }
235
236    /// Split one resource into two. Both the returned resource and self have half of the original
237    /// fraction.
238    pub proof fn split(tracked &mut self) -> (tracked result: Self)
239        ensures
240            final(self).id() == old(self).id(),
241            result.id() == final(self).id(),
242            final(self)@ == old(self)@,
243            result@ == old(self)@,
244            final(self).frac() == old(self).frac() / 2 as real,
245            result.frac() == old(self).frac() / 2 as real,
246    {
247        self.bounded();
248        self.split_to(self.frac() / 2 as real)
249    }
250
251    /// Combine two resources, summing their quantities.
252    pub proof fn combine(tracked &mut self, tracked other: Self)
253        requires
254            old(self).id() == other.id(),
255        ensures
256            final(self).id() == old(self).id(),
257            final(self)@ == old(self)@,
258            final(self)@ == other@,
259            final(self).frac() == old(self).frac() + other.frac(),
260    {
261        self.bounded();
262        let tracked mut mself = Self::dummy();
263        tracked_swap(self, &mut mself);
264        use_type_invariant(&mself);
265        use_type_invariant(&other);
266        let tracked mut r = mself.r;
267        r.validate_2(&other.r);
268        *self = Self { r: r.join(other.r) };
269    }
270
271    /// Update the value of the resource. This requires having ALL the permissions,
272    pub proof fn update(tracked &mut self, v: T)
273        requires
274            old(self).frac() == (1 as real),
275        ensures
276            final(self).id() == old(self).id(),
277            final(self)@ == v,
278            final(self).frac() == old(self).frac(),
279    {
280        self.bounded();
281        let tracked mut mself = Self::dummy();
282        tracked_swap(self, &mut mself);
283        use_type_invariant(&mself);
284        let tracked mut r = mself.r;
285        let f = FractionalCarrier {
286            left: FractionRA::Frac(1 as real),
287            right: AgreementRA::Agree(v),
288        };
289        lemma_whole_fraction_has_no_frame(r.value().left);
290        *self = Self { r: r.update(f) };
291    }
292
293    /// Update the value of the token. This requires having ALL the permissions (i.e., a fractional
294    /// authority of 1),
295    pub proof fn update_with(tracked &mut self, tracked other: &mut Self, v: T)
296        requires
297            old(self).id() == old(other).id(),
298            old(self).frac() + old(other).frac() == 1 as real,
299        ensures
300            final(self).id() == old(self).id(),
301            final(other).id() == old(other).id(),
302            final(self).frac() == old(self).frac(),
303            final(other).frac() == old(other).frac(),
304            old(self)@ == old(other)@,
305            final(self)@ == v,
306            final(other)@ == v,
307    {
308        let ghost other_frac = other.frac();
309        other.bounded();
310
311        let tracked mut xother = Self::dummy();
312        tracked_swap(other, &mut xother);
313        self.bounded();
314        self.combine(xother);
315        self.update(v);
316
317        let tracked mut xother = self.split_to(other_frac);
318        tracked_swap(other, &mut xother);
319    }
320
321    /// Allowed values for a resource's fractional component.
322    pub proof fn bounded(tracked &self)
323        ensures
324            (0 as real) < self.frac() <= (1 as real),
325    {
326        use_type_invariant(self);
327        self.r.validate()
328    }
329
330    /// Obtain an arbitrary resource with no information about it.
331    /// Useful if you need a well-typed placeholder.
332    pub proof fn dummy() -> (tracked result: Self) {
333        Self::new(arbitrary())
334    }
335}
336
337} // verus!
vstd/resource/frac.rs

vstd/resource/
frac.rs
