vstd_extra/resource/pcm/
excl.rs

1//! This module defines an exclusive PCM.
2//!
3//! For Iris definition, see:
4//! <https://gitlab.mpi-sws.org/iris/iris/-/blob/master/iris/algebra/excl.v>
5use vstd::pcm::PCM;
6use vstd::prelude::*;
7
8verus! {
9
10/// Exclusive 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 ExclR<A> {
15    Unit,
16    /// Exclusive ownership of a value.
17    Excl(A),
18    /// Invalid state.
19    ExclInvalid,
20}
21
22impl<A> PCM for ExclR<A> {
23    open spec fn valid(self) -> bool {
24        self !is ExclInvalid
25    }
26
27    // Compositio of two non-unit elements is always invalid.
28    open spec fn op(self, other: Self) -> Self {
29        match (self, other) {
30            (ExclR::Unit, x) => x,
31            (x, ExclR::Unit) => x,
32            _ => ExclR::ExclInvalid,
33        }
34    }
35
36    open spec fn unit() -> Self {
37        ExclR::Unit
38    }
39
40    proof fn closed_under_incl(a: Self, b: Self) {
41    }
42
43    proof fn commutative(a: Self, b: Self) {
44    }
45
46    proof fn associative(a: Self, b: Self, c: Self) {
47    }
48
49    proof fn op_unit(a: Self) {
50    }
51
52    proof fn unit_valid() {
53    }
54}
55
56} // verus!
vstd_extra/resource/pcm/excl.rs

vstd_extra/resource/pcm/
excl.rs
