vstd/resource/
relations.rs

1use super::super::prelude::*;
2use super::algebra::ResourceAlgebra;
3use super::pcm::PCM;
4
5verus! {
6
7/// The preorder relation.
8/// `incl(a, b)` (or a ≼ b) means that there is some `c` such that `a · c == b`
9pub open spec fn incl<RA: ResourceAlgebra>(a: RA, b: RA) -> bool {
10    exists|c| RA::op(a, c) == b
11}
12
13pub open spec fn conjunct_shared<RA: ResourceAlgebra>(a: RA, b: RA, c: RA) -> bool {
14    forall|p: RA| p.valid() && incl(a, p) && incl(b, p) ==> #[trigger] incl(c, p)
15}
16
17/// A frame preserving update is an update of a value from `a --> b` such that every value `c`
18/// that could compose with `a` (also called the frame) can still compose with `b`.
19pub open spec fn frame_preserving_update<P: PCM>(a: P, b: P) -> bool {
20    forall|c| #![trigger P::op(a, c), P::op(b, c)] P::op(a, c).valid() ==> P::op(b, c).valid()
21}
22
23/// A nondeterministic version of a [`frame_preserving_update`].
24pub open spec fn frame_preserving_update_nondeterministic<P: PCM>(a: P, bs: Set<P>) -> bool {
25    forall|c|
26        #![trigger P::op(a, c)]
27        P::op(a, c).valid() ==> exists|b| #[trigger] bs.contains(b) && P::op(b, c).valid()
28}
29
30/// A frame preserving update with support for resource algebras.
31/// See [`frame_preserving_update`] for more details.
32/// The difference lies in the fact that for [`PCM`]s there is always a unit
33///
34pub open spec fn frame_preserving_update_opt<RA: ResourceAlgebra>(a: RA, b: RA) -> bool {
35    forall|c|
36        #![trigger Option::<RA>::op(Some(a), c), Option::<RA>::op(Some(b), c)]
37        Option::<RA>::op(Some(a), c).valid() ==> Option::<RA>::op(Some(b), c).valid()
38}
39
40/// A nondeterministic version of a [`frame_preserving_update_opt`].
41pub open spec fn frame_preserving_update_nondeterministic_opt<RA: ResourceAlgebra>(
42    a: RA,
43    bs: Set<RA>,
44) -> bool {
45    forall|c|
46        #![trigger Option::<RA>::op(Some(a), c)]
47        Option::<RA>::op(Some(a), c).valid() ==> exists|b| #[trigger]
48            bs.contains(b) && Option::<RA>::op(Some(b), c).valid()
49}
50
51/// The set of values such that can be created by composing an element of `s` with `t`.
52pub open spec fn set_op<RA: ResourceAlgebra>(s: Set<RA>, t: RA) -> Set<RA> {
53    Set::new(|v| exists|q| s.contains(q) && v == RA::op(q, t))
54}
55
56pub proof fn lemma_incl_transitive<RA: ResourceAlgebra>(a: RA, b: RA, c: RA)
57    requires
58        incl(a, b),
59        incl(b, c),
60    ensures
61        incl(a, c),
62{
63    let ax = choose|ax| RA::op(a, ax) == b;
64    let bx = choose|bx| RA::op(b, bx) == c;
65    assert(RA::op(RA::op(a, ax), bx) == c);
66    RA::associative(a, ax, bx);
67    assert(RA::op(a, RA::op(ax, bx)) == c);
68}
69
70pub proof fn lemma_frame_preserving_opt<RA: ResourceAlgebra>(a: RA, b: RA)
71    requires
72        frame_preserving_update_opt::<RA>(a, b),
73    ensures
74        frame_preserving_update::<Option<RA>>(Some(a), Some(b)),
75{
76}
77
78pub proof fn lemma_frame_preserving_update_nondeterministic_opt<RA: ResourceAlgebra>(
79    a: RA,
80    bs: Set<RA>,
81)
82    requires
83        frame_preserving_update_nondeterministic_opt::<RA>(a, bs),
84    ensures
85        frame_preserving_update_nondeterministic::<Option<RA>>(Some(a), bs.map(|b| Some(b))),
86{
87    broadcast use super::super::set::group_set_axioms;
88
89    let bs_mapped = bs.map(|b| Some(b));
90    assert forall|c|
91        #![trigger Option::<RA>::op(Some(a), c)]
92        Option::<RA>::op(Some(a), c).valid() implies exists|b| #[trigger]
93        bs_mapped.contains(b) && Option::<RA>::op(b, c).valid() by {
94        let b = choose|b| #[trigger] bs.contains(b) && Option::<RA>::op(Some(b), c).valid();
95        assert(bs_mapped.contains(Some(b)));
96    }
97}
98
99} // verus!
vstd/resource/relations.rs

vstd/resource/
relations.rs
