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_frame_preserving_opt<RA: ResourceAlgebra>(a: RA, b: RA)
57    requires
58        frame_preserving_update_opt::<RA>(a, b),
59    ensures
60        frame_preserving_update::<Option<RA>>(Some(a), Some(b)),
61{
62}
63
64pub proof fn lemma_frame_preserving_update_nondeterministic_opt<RA: ResourceAlgebra>(
65    a: RA,
66    bs: Set<RA>,
67)
68    requires
69        frame_preserving_update_nondeterministic_opt::<RA>(a, bs),
70    ensures
71        frame_preserving_update_nondeterministic::<Option<RA>>(Some(a), bs.map(|b| Some(b))),
72{
73    broadcast use super::super::set::group_set_axioms;
74
75    let bs_mapped = bs.map(|b| Some(b));
76    assert forall|c|
77        #![trigger Option::<RA>::op(Some(a), c)]
78        Option::<RA>::op(Some(a), c).valid() implies exists|b| #[trigger]
79        bs_mapped.contains(b) && Option::<RA>::op(b, c).valid() by {
80        let b = choose|b| #[trigger] bs.contains(b) && Option::<RA>::op(Some(b), c).valid();
81        assert(bs_mapped.contains(Some(b)));
82    }
83}
84
85} // verus!
vstd/resource/relations.rs

vstd/resource/
relations.rs
