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

vstd/resource/
frac.rs
