vstd/resource/
agree.rs

1use super::super::prelude::*;
2use super::algebra::Resource;
3use super::algebra::ResourceAlgebra;
4
5verus! {
6
7/// The Agreement resource algebra
8///
9/// This resource algebra allows one to express that multiple parties can _agree_ on a chosen value
10/// This is mainly useful to show that if two resources are `Agree` then they must point to the
11/// same value (see [`lemma_agree`]):
12/// ```
13pub enum AgreementRA<T> {
14    Agree(T),
15    Invalid,
16}
17
18impl<T> ResourceAlgebra for AgreementRA<T> {
19    open spec fn valid(self) -> bool {
20        match self {
21            AgreementRA::Invalid => false,
22            _ => true,
23        }
24    }
25
26    open spec fn op(a: Self, b: Self) -> Self {
27        match (a, b) {
28            (AgreementRA::Agree(a), AgreementRA::Agree(b)) if a == b => AgreementRA::Agree(a),
29            _ => AgreementRA::Invalid,
30        }
31    }
32
33    proof fn associative(a: Self, b: Self, c: Self) {
34    }
35
36    proof fn commutative(a: Self, b: Self) {
37    }
38
39    proof fn valid_op(a: Self, b: Self) {
40    }
41}
42
43impl<T> AgreementRA<T> {
44    pub open spec fn view(self) -> T {
45        self->Agree_0
46    }
47}
48
49pub proof fn lemma_agree<T>(
50    tracked a: &Resource<AgreementRA<T>>,
51    tracked b: &Resource<AgreementRA<T>>,
52)
53    requires
54        a.loc() == b.loc(),
55    ensures
56        a.value()@ == b.value()@,
57{
58    a.as_ref().join_shared(&b.as_ref()).validate();
59}
60
61} // verus!
vstd/resource/agree.rs

vstd/resource/
agree.rs
