vstd/resource/
option.rs

1use super::super::prelude::*;
2use super::algebra::ResourceAlgebra;
3use super::pcm::PCM;
4use super::relations::*;
5
6verus! {
7
8impl<RA: ResourceAlgebra> ResourceAlgebra for Option<RA> {
9    /// Whether an element is valid
10    open spec fn valid(self) -> bool {
11        match self {
12            Some(v) => v.valid(),
13            None => true,
14        }
15    }
16
17    /// Compose two elements
18    open spec fn op(a: Self, b: Self) -> Self {
19        match (a, b) {
20            (Some(a), Some(b)) => Some(RA::op(a, b)),
21            (None, _) => b,
22            (_, None) => a,
23        }
24    }
25
26    /// The operation is associative
27    proof fn associative(a: Self, b: Self, c: Self) {
28        match (a, b, c) {
29            (Some(a), Some(b), Some(c)) => RA::associative(a, b, c),
30            (_, _, _) => {},
31        }
32    }
33
34    /// The operation is commutative
35    proof fn commutative(a: Self, b: Self) {
36        match (a, b) {
37            (Some(a), Some(b)) => RA::commutative(a, b),
38            (_, _) => {},
39        }
40    }
41
42    /// The operation is closed under inclusion
43    /// (i.e., if the result of the operation is valid then its parts are also valid)
44    proof fn valid_op(a: Self, b: Self) {
45        match (a, b) {
46            (Some(a), Some(b)) => RA::valid_op(a, b),
47            (_, _) => {},
48        }
49    }
50}
51
52impl<RA: ResourceAlgebra> PCM for Option<RA> {
53    open spec fn unit() -> Self {
54        None
55    }
56
57    /// The core of an element `a` is, by definition, some other element `x`
58    /// such that `a op x = a`
59    proof fn op_unit(self) {
60    }
61
62    /// The unit is always a valid element
63    proof fn unit_valid() {
64    }
65}
66
67pub proof fn lemma_incl_opt<RA: ResourceAlgebra>(a: RA, b: RA)
68    requires
69        incl::<RA>(a, b),
70    ensures
71        incl::<Option<RA>>(Some(a), Some(b)),
72{
73    let c = choose|x| RA::op(a, x) == b;
74    assert(Option::<RA>::op(Some(a), Some(c)) == Some(b));
75}
76
77pub proof fn lemma_incl_opt_rev<RA: ResourceAlgebra>(a: RA, b: RA)
78    requires
79        incl::<Option<RA>>(Some(a), Some(b)),
80    ensures
81        incl::<RA>(a, b) || a == b,
82{
83    let c = choose|x| Option::<RA>::op(Some(a), x) == Some(b);
84    if c is None {
85        Some(a).op_unit();
86    }
87}
88
89pub proof fn lemma_set_op_opt<RA: ResourceAlgebra>(s: Set<RA>, t: RA)
90    ensures
91        set_op(s, t).map(|b| Some(b)) == set_op(s.map(|x| Some(x)), Some(t)),
92{
93    broadcast use super::super::set::group_set_axioms;
94
95    let s_mapped = s.map(|x| Some(x));
96    let original = set_op(s, t);
97    let map_after = original.map(|b| Some(b));
98    let map_before = set_op(s_mapped, Some(t));
99
100    assert forall|v| map_after.contains(v) implies map_before.contains(v) by {
101        let q = choose|q| #[trigger] s.contains(q) && v->Some_0 == RA::op(q, t);
102        assert(s_mapped.contains(Some(q)));
103    }
104
105    assert forall|v| map_before.contains(v) implies map_after.contains(v) by {
106        let q = choose|q| #[trigger] s_mapped.contains(q) && v == Option::<RA>::op(q, Some(t));
107        assert(original.contains(v->Some_0));
108    }
109}
110
111} // verus!
vstd/resource/option.rs

vstd/resource/
option.rs
