vstd_extra/resource/pcm/
agree.rs

1//! This module defines the Agreement PCM.
2//!
3//! For Iris definition, see:
4//! <https://gitlab.mpi-sws.org/iris/iris/-/blob/master/iris/algebra/agree.v>
5use vstd::pcm::PCM;
6use vstd::prelude::*;
7
8verus! {
9
10/// Agreement PCM
11///
12/// In modern Iris, it uses CMRA instead of PCM, which uses a core for every element instead of a unit element.
13/// Here we add a unit element to stick to the PCM definition.
14pub tracked enum AgreeR<A> {
15    Unit,
16    /// Agreement on a value.
17    Agree(A),
18    /// Invalid state.
19    AgreeInvalid,
20}
21
22impl<A: PartialEq> PCM for AgreeR<A> {
23    open spec fn valid(self) -> bool {
24        self !is AgreeInvalid
25    }
26
27    /// Composition: two agreeing values must be equal.
28    open spec fn op(self, other: Self) -> Self {
29        match (self, other) {
30            (AgreeR::Unit, x) => x,
31            (x, AgreeR::Unit) => x,
32            (AgreeR::Agree(a), AgreeR::Agree(b)) => {
33                if a == b {
34                    AgreeR::Agree(a)
35                } else {
36                    AgreeR::AgreeInvalid
37                }
38            },
39            _ => AgreeR::AgreeInvalid,
40        }
41    }
42
43    open spec fn unit() -> Self {
44        AgreeR::Unit
45    }
46
47    proof fn closed_under_incl(a: Self, b: Self) {
48    }
49
50    proof fn commutative(a: Self, b: Self) {
51    }
52
53    proof fn associative(a: Self, b: Self, c: Self) {
54    }
55
56    proof fn op_unit(a: Self) {
57    }
58
59    proof fn unit_valid() {
60    }
61}
62
63} // verus!
vstd_extra/resource/pcm/agree.rs

vstd_extra/resource/pcm/
agree.rs
