vstd/resource/
auth.rs

1use super::super::prelude::*;
2use super::algebra::ResourceAlgebra;
3use super::exclusive::ExclusiveRA;
4#[cfg(verus_keep_ghost)]
5use super::option::lemma_incl_opt_rev;
6use super::pcm::PCM;
7#[cfg(verus_keep_ghost)]
8use super::relations::incl;
9#[cfg(verus_keep_ghost)]
10use super::relations::lemma_incl_transitive;
11
12verus! {
13
14pub struct AuthRA<RA: ResourceAlgebra> {
15    pub auth: Option<ExclusiveRA<RA>>,
16    pub frac: RA,
17}
18
19proof fn lemma_incl_valid<RA: ResourceAlgebra>(a: RA, b: RA)
20    requires
21        incl(a, b),
22        b.valid(),
23    ensures
24        a.valid(),
25{
26    let c = choose|c| RA::op(a, c) == b;
27    RA::valid_op(a, c);
28}
29
30impl<RA: ResourceAlgebra> ResourceAlgebra for AuthRA<RA> {
31    open spec fn valid(self) -> bool {
32        match self.auth {
33            None => self.frac.valid(),
34            Some(ExclusiveRA::Exclusive(a)) => a.valid() && incl(self.frac, a),
35            Some(ExclusiveRA::Invalid) => false,
36        }
37    }
38
39    open spec fn op(a: Self, b: Self) -> Self {
40        let auth = Option::<ExclusiveRA::<RA>>::op(a.auth, b.auth);
41        let frac = RA::op(a.frac, b.frac);
42        AuthRA { auth, frac }
43    }
44
45    proof fn associative(a: Self, b: Self, c: Self) {
46        Option::<ExclusiveRA::<RA>>::associative(a.auth, b.auth, c.auth);
47        RA::associative(a.frac, b.frac, c.frac);
48    }
49
50    proof fn commutative(a: Self, b: Self) {
51        Option::<ExclusiveRA::<RA>>::commutative(a.auth, b.auth);
52        RA::commutative(a.frac, b.frac);
53    }
54
55    proof fn valid_op(a: Self, b: Self) {
56        let op = Self::op(a, b);
57        match op.auth {
58            None => {
59                RA::valid_op(a.frac, b.frac);
60            },
61            Some(auth) => {
62                lemma_incl_valid(op.frac, auth->Exclusive_0);
63
64                RA::valid_op(a.frac, b.frac);
65                Option::<ExclusiveRA::<RA>>::valid_op(a.auth, b.auth);
66                if a.auth is Some {
67                    lemma_incl_opt_rev(a.auth->Some_0, auth);
68                    if a.auth->Some_0 == auth {
69                        lemma_incl_transitive(a.frac, op.frac, a.auth->Some_0->Exclusive_0);
70                    }
71                }
72            },
73        }
74    }
75}
76
77impl<P: PCM> PCM for AuthRA<P> {
78    open spec fn unit() -> Self {
79        AuthRA { auth: None, frac: P::unit() }
80    }
81
82    proof fn op_unit(self) {
83        Option::<ExclusiveRA::<P>>::op_unit(self.auth);
84        P::op_unit(self.frac);
85    }
86
87    proof fn unit_valid() {
88        Option::<ExclusiveRA::<P>>::unit_valid();
89        P::unit_valid();
90    }
91}
92
93} // verus!
vstd/resource/auth.rs

vstd/resource/
auth.rs
