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 struct FracStorage<T> {
19    r: 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: 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            self.id() == old(self).id(),
69            self.resource() == old(self).resource(),
70            r.resource() == old(self).resource(),
71            r.id() == old(self).id(),
72            r.frac() + 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(tracked r: &mut Option<StorageResource<(), T, FracP<T>>>) -> (tracked res:
80        Self)
81        requires
82            *old(r) is Some,
83            old(r)->Some_0.value() is Frac,
84            old(r)->Some_0.value().frac() > 0.0real,
85            old(r)->Some_0.value().frac() <= 1.0real,
86        ensures
87            *r is Some,
88            r->Some_0.value() is Frac,
89            r->Some_0.value().frac() > 0.0real,
90            r->Some_0.value().frac() <= 1.0real,
91            res.id() == old(r)->Some_0.loc(),
92            r->Some_0.loc() == old(r)->Some_0.loc(),
93            r->Some_0.value().value() == old(r)->Some_0.value().value(),
94            res.resource() == old(r)->Some_0.value().value(),
95            res.frac() + r->Some_0.value().frac() == old(r)->Some_0.value().frac(),
96    {
97        let tracked mut storage_resource = r.tracked_take();
98        let frac = storage_resource.value().frac();
99        let half_frac = frac / 2.0real;
100        let m = FracP::construct_frac(half_frac, storage_resource.value().value());
101        let tracked (resource_1, resource_2) = storage_resource.split(m, m);
102        *r = Some(resource_1);
103        FracStorage { r: Some(resource_2) }
104    }
105
106    /// Obtain shared access to the underlying resource.
107    pub proof fn borrow(tracked &self) -> (tracked s: &T)
108        ensures
109            *s == self.resource(),
110    {
111        use_type_invariant(self);
112        let m = Map::<(), T>::empty().insert((), self.resource());
113        self.protocol_monoid().lemma_guards();
114        let tracked resource = StorageResource::guard(self.r.tracked_borrow(), m);
115        resource.tracked_borrow(())
116    }
117}
118
119} // verus!
vstd_extra/resource/ghost_resource/frac.rs

vstd_extra/resource/ghost_resource/
frac.rs
