vstd_extra/resource/ghost_resource/
frac.rs

1//! Real-based fractional ghost resource.
2use vstd::map::*;
3use vstd::pcm::Loc;
4use vstd::prelude::*;
5use vstd::storage_protocol::*;
6
7use crate::resource::storage_protocol::frac::*;
8
9verus! {
10
11///`FracStorage` define the actual storage resource that can be split
12/// into arbitrary finite pieces for shared read access.
13///
14/// It can be seen as a real-based re-implementation of
15/// `Frac`(https://verus-lang.github.io/verus/verusdoc/vstd/tokens/frac/struct.FracGhost.html).
16use vstd::map::*;
17
18pub tracked struct FracStorage<T> {
19    tracked r: Tracked<Option<StorageResource<(), T, FracP<T>>>>,
20}
21
22impl<T> FracStorage<T> {
23    #[verifier::type_invariant]
24    spec fn type_inv(self) -> bool {
25        &&& self.r@ is Some
26        &&& self.protocol_monoid() is Frac
27        &&& 0.0real < self.frac() && self.frac() <= 1.0real
28    }
29
30    pub closed spec fn storage_resource(self) -> StorageResource<(), T, FracP<T>> {
31        self.r@->Some_0
32    }
33
34    pub closed spec fn id(self) -> Loc {
35        self.storage_resource().loc()
36    }
37
38    pub closed spec fn protocol_monoid(self) -> FracP<T> {
39        self.storage_resource().value()
40    }
41
42    pub open spec fn resource(self) -> T {
43        self.protocol_monoid().value()
44    }
45
46    pub closed spec fn frac(self) -> real {
47        self.protocol_monoid().frac()
48    }
49
50    pub open spec fn has_full_frac(self) -> bool {
51        self.frac() == 1.0real
52    }
53
54    /// Allocate a new fractional storage resource with full permission.
55    pub proof fn alloc(tracked v: T) -> (tracked res: Self)
56        ensures
57            res.has_full_frac(),
58    {
59        let tracked mut m = Map::<(), T>::tracked_empty();
60        m.tracked_insert((), v);
61        let tracked resource = StorageResource::alloc(FracP::new(v), m);
62        FracStorage { r: Tracked(Some(resource)) }
63    }
64
65    /// Split one token into two tokens whose quantities sum to the original.
66    pub proof fn split(tracked &mut self) -> (tracked r: FracStorage<T>)
67        ensures
68            final(self).id() == old(self).id(),
69            final(self).resource() == old(self).resource(),
70            r.resource() == old(self).resource(),
71            r.id() == old(self).id(),
72            r.frac() + final(self).frac() == old(self).frac(),
73    {
74        use_type_invariant(&*self);
75        Self::split_helper(&mut self.r)
76    }
77
78    /// Avoid breaking the type invariant.
79    proof fn split_helper(
80        tracked r: &mut Tracked<Option<StorageResource<(), T, FracP<T>>>>,
81    ) -> (tracked res: Self)
82        requires
83            old(r)@ is Some,
84            old(r)@->Some_0.value() is Frac,
85            old(r)@->Some_0.value().frac() > 0.0real,
86            old(r)@->Some_0.value().frac() <= 1.0real,
87        ensures
88            final(r)@ is Some,
89            final(r)@->Some_0.value() is Frac,
90            final(r)@->Some_0.value().frac() > 0.0real,
91            final(r)@->Some_0.value().frac() <= 1.0real,
92            res.id() == old(r)@->Some_0.loc(),
93            final(r)@->Some_0.loc() == old(r)@->Some_0.loc(),
94            final(r)@->Some_0.value().value() == old(r)@->Some_0.value().value(),
95            res.resource() == old(r)@->Some_0.value().value(),
96            res.frac() + final(r)@->Some_0.value().frac() == old(r)@->Some_0.value().frac(),
97    {
98        let tracked mut storage_resource = r.borrow_mut().tracked_take();
99        let frac = storage_resource.value().frac();
100        let half_frac = frac / 2.0real;
101        let m = FracP::construct_frac(half_frac, storage_resource.value().value());
102        let tracked (resource_1, resource_2) = storage_resource.split(m, m);
103        **r = Some(resource_1);
104        FracStorage { r: Tracked(Some(resource_2)) }
105    }
106
107    /// Obtain shared access to the underlying resource.
108    pub proof fn borrow(tracked &self) -> (tracked s: &T)
109        ensures
110            *s == self.resource(),
111    {
112        use_type_invariant(self);
113        let m = Map::<(), T>::empty().insert((), self.resource());
114        self.protocol_monoid().lemma_guards();
115        let tracked resource = StorageResource::guard(self.r.borrow().tracked_borrow(), m);
116        resource.tracked_borrow(())
117    }
118}
119
120} // verus!
vstd_extra/resource/ghost_resource/frac.rs

vstd_extra/resource/ghost_resource/
frac.rs
