vstd_extra/resource/storage_protocol/
frac.rs

1//! Real-based fractional permissions storage protocol.
2use vstd::map::*;
3use vstd::pcm::Loc;
4use vstd::prelude::*;
5use vstd::storage_protocol::*;
6
7verus! {
8
9broadcast use group_map_axioms;
10
11/// The fractional protocol monoid.
12#[verifier::ext_equal]
13pub ghost enum FracP<T> {
14    Unit,
15    Frac(real, T),
16    Invalid,
17}
18
19impl<T> Protocol<(), T> for FracP<T> {
20    open spec fn op(self, other: Self) -> Self {
21        match (self, other) {
22            (FracP::Unit, x) => x,
23            (x, FracP::Unit) => x,
24            (FracP::Frac(q1, v1), FracP::Frac(q2, v2)) => {
25                if v1 == v2 && 0.0real < q1 && 0.0real < q2 && q1 + q2 <= 1.0real {
26                    FracP::Frac(q1 + q2, v1)
27                } else {
28                    FracP::Invalid
29                }
30            },
31            _ => FracP::Invalid,
32        }
33    }
34
35    open spec fn rel(self, s: Map<(), T>) -> bool {
36        match self {
37            FracP::Frac(q, v) => {
38                &&& s.contains_key(())
39                &&& s[()] == v
40                &&& q == 1.0real
41            },
42            _ => false,
43        }
44    }
45
46    open spec fn unit() -> Self {
47        FracP::Unit
48    }
49
50    proof fn commutative(a: Self, b: Self) {
51    }
52
53    proof fn associative(a: Self, b: Self, c: Self) {
54    }
55
56    proof fn op_unit(a: Self) {
57    }
58}
59
60impl<T> FracP<T> {
61    pub open spec fn frac(self) -> real {
62        match self {
63            FracP::Frac(q, _) => q,
64            _ => 0.0real,
65        }
66    }
67
68    pub open spec fn new(v: T) -> Self {
69        FracP::Frac(1.0real, v)
70    }
71
72    pub open spec fn construct_frac(q: real, v: T) -> Self {
73        FracP::Frac(q, v)
74    }
75
76    pub open spec fn value(self) -> T
77        recommends
78            self is Frac,
79    {
80        match self {
81            FracP::Frac(_, v) => v,
82            _ => arbitrary(),
83        }
84    }
85
86    pub proof fn lemma_guards(self)
87        requires
88            self is Frac,
89        ensures
90            guards::<(), T, Self>(self, map![() => self.value()]),
91    {
92    }
93}
94
95} // verus!
vstd_extra/resource/storage_protocol/frac.rs

vstd_extra/resource/storage_protocol/
frac.rs
