vstd_extra/resource/storage/
frac.rs

1//! This module defines the real-based fractional permissions storage protocol.
2//!
3//! - `FracP` defines the basic fractional protocol monoid.
4//! - `FracStorage` define the actual storage resource that can be split
5//! into arbitrary finite pieces for shared read access, it can be seen
6//! as a real-based re-implemetation of `Frac`(https://verus-lang.github.io/verus/verusdoc/vstd/tokens/frac/struct.FracGhost.html).
7use crate::ownership::Inv;
8use vstd::map::*;
9use vstd::pcm::Loc;
10use vstd::prelude::*;
11use vstd::storage_protocol::*;
12
13verus! {
14
15broadcast use group_map_axioms;
16
17/// The fractional protocol monoid
18#[verifier::ext_equal]
19pub tracked enum FracP<T> {
20    Unit,
21    Frac(real, T),
22    Invalid,
23}
24
25impl <T> Protocol<(),T> for FracP<T> {
26    open spec fn op(self,other: Self) -> Self {
27        match (self,other) {
28            (FracP::Unit, x) => x,
29            (x, FracP::Unit) => x,
30            (FracP::Frac(q1, v1), FracP::Frac(q2, v2)) => {
31                if v1 == v2 && 0.0real < q1 && 0.0real < q2 && q1 + q2 <= 1.0real {
32                    FracP::Frac(q1 + q2, v1)
33                } else {
34                    FracP::Invalid
35                }
36            }
37            _ => FracP::Invalid,
38        }
39    }
40
41    open spec fn rel(self, s:Map<(),T>) -> bool {
42        match self {
43            FracP::Frac(q, v) => {
44                &&& s.contains_key(())
45                &&& s[()] == v
46                &&& q == 1.0real
47            }
48            _ => false,
49        }
50    }
51
52    open spec fn unit() -> Self {
53        FracP::Unit
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
66impl<T> FracP<T> {
67    pub open spec fn frac(self) -> real {
68        match self {
69            FracP::Frac(q, _) => q,
70            _ => 0.0real,
71        }
72    }
73
74    pub open spec fn new(v:T) -> Self
75    {
76        FracP::Frac(1.0real, v)
77    }
78
79    pub open spec fn construct_frac(q:real, v:T) -> Self
80    {
81        FracP::Frac(q, v)
82    }
83
84    pub open spec fn value(self) -> T
85    recommends
86        self is Frac,
87    {
88        match self {
89            FracP::Frac(_, v) => v,
90            _ => arbitrary()
91        }
92    }
93
94    pub proof fn lemma_guards(self)
95    requires
96        self is Frac,
97    ensures
98        guards::<(),T,Self>(self,map![() => self.value()]),
99    {
100    }
101}
102
103/// The authoritative fractional storage resource.
104pub struct FracStorage<T> {
105    r: Option<StorageResource<(), T, FracP<T>>>,
106}
107
108impl<T> FracStorage<T> {
109    #[verifier::type_invariant]
110    spec fn type_inv(self) -> bool {
111        &&& self.r is Some
112        &&& self.protocol_monoid() is Frac
113        &&& 0.0real < self.frac() && self.frac() <= 1.0real
114    }
115
116    pub closed spec fn storage_resource(self) -> StorageResource<(), T, FracP<T>> {
117        self.r -> Some_0
118    }
119
120    pub closed spec fn id(self) -> Loc{
121        self.storage_resource().loc()
122    }
123
124    pub closed spec fn protocol_monoid(self) -> FracP<T> {
125        self.storage_resource().value()
126    }
127
128    pub open spec fn resource(self) -> T {
129        self.protocol_monoid().value()
130    }
131
132    pub closed spec fn frac(self) -> real {
133        self.protocol_monoid().frac()
134    }
135
136    pub open spec fn has_full_frac(self) -> bool {
137        self.frac() == 1.0real
138    }
139
140    /// Allocate a new fractional storage resource with full permission.
141    pub proof fn new(tracked v:T) -> (tracked res: Self)
142    ensures
143        res.has_full_frac(),
144    {
145        let tracked mut m = Map::<(),T>::tracked_empty();
146        m.tracked_insert((), v);
147        let tracked resource = StorageResource::alloc(FracP::new(v), m);
148        FracStorage { r: Some(resource) }
149    }
150
151    /// Split one token into two tokens whose quantities sum to the original.
152    pub proof fn split(tracked &mut self) -> (tracked r: FracStorage<T>)
153    ensures
154        self.id() == old(self).id(),
155        self.resource() == old(self).resource(),
156        r.resource() == old(self).resource(),
157        r.id() == old(self).id(),
158        r.frac() + self.frac() == old(self).frac(),
159    {
160        use_type_invariant(&*self);
161        Self::split_helper(&mut self.r)
162    }
163
164    /// Avoid breaking the type invariant.
165    proof fn split_helper(tracked r: &mut Option<StorageResource<(),T,FracP<T>>>) -> (tracked res: Self)
166    requires
167        *old(r) is Some,
168        old(r)->Some_0.value() is Frac,
169        old(r)->Some_0.value().frac() > 0.0real,
170        old(r)->Some_0.value().frac() <= 1.0real,
171    ensures
172        *r is Some,
173        r->Some_0.value() is Frac,
174        r->Some_0.value().frac() > 0.0real,
175        r->Some_0.value().frac() <= 1.0real,
176        res.id() == old(r)->Some_0.loc(),
177        r->Some_0.loc() == old(r)->Some_0.loc(),
178        r->Some_0.value().value() == old(r)->Some_0.value().value(),
179        res.resource() == old(r)->Some_0.value().value(),
180        res.frac() + r->Some_0.value().frac() == old(r)->Some_0.value().frac(),
181    {
182        let tracked mut storage_resource = r.tracked_take();
183        let frac = storage_resource.value().frac();
184        let half_frac = frac / 2.0real;
185        let m = FracP::construct_frac(half_frac, storage_resource.value().value());
186        let tracked (resource_1, resource_2) = storage_resource.split(m,m);
187        *r = Some(resource_1);
188        FracStorage { r: Some(resource_2) }
189    }
190
191    /// Obtain shared access to the underlying resource.
192    pub proof fn borrow(tracked &self) -> (tracked s: &T)
193    ensures
194        *s == self.resource(),
195    {
196        use_type_invariant(self);
197        let m = Map::<(),T>::empty().insert((), self.resource());
198        self.protocol_monoid().lemma_guards();
199        let tracked resource = StorageResource::guard(self.r.tracked_borrow(), m);
200        resource.tracked_borrow(())
201    }
202}
203
204}
vstd_extra/resource/storage/frac.rs

vstd_extra/resource/storage/
frac.rs
