vstd_extra/resource/pcm/
csum.rs

1//! Csum PCM
2//!
3//! For Iris definition, see:
4//! <https://gitlab.mpi-sws.org/iris/iris/-/blob/master/iris/algebra/csum.v>
5use vstd::pcm::PCM;
6use vstd::prelude::*;
7
8verus! {
9
10/// Csum 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 CsumR<A, B> {
15    Unit,
16    Cinl(A),
17    Cinr(B),
18    CsumInvalid,
19}
20
21impl<A: PCM, B: PCM> PCM for CsumR<A, B> {
22    open spec fn valid(self) -> bool {
23        match self {
24            CsumR::Unit => true,
25            CsumR::Cinl(a) => A::valid(a),
26            CsumR::Cinr(b) => B::valid(b),
27            CsumR::CsumInvalid => false,
28        }
29    }
30
31    open spec fn op(self, other: Self) -> Self {
32        match (self, other) {
33            (CsumR::Unit, x) => x,
34            (x, CsumR::Unit) => x,
35            (CsumR::Cinl(a1), CsumR::Cinl(a2)) => CsumR::Cinl(A::op(a1, a2)),
36            (CsumR::Cinr(b1), CsumR::Cinr(b2)) => CsumR::Cinr(B::op(b1, b2)),
37            _ => CsumR::CsumInvalid,
38        }
39    }
40
41    open spec fn unit() -> Self {
42        CsumR::Unit
43    }
44
45    proof fn closed_under_incl(a: Self, b: Self) {
46        if Self::op(a, b).valid() {
47            match (a, b) {
48                (CsumR::Cinl(a1), CsumR::Cinl(a2)) => {
49                    A::closed_under_incl(a1, a2);
50                },
51                (CsumR::Cinr(b1), CsumR::Cinr(b2)) => {
52                    B::closed_under_incl(b1, b2);
53                },
54                _ => {},
55            }
56        }
57    }
58
59    proof fn commutative(a: Self, b: Self) {
60        match (a, b) {
61            (CsumR::Cinl(a1), CsumR::Cinl(a2)) => {
62                A::commutative(a1, a2);
63            },
64            (CsumR::Cinr(b1), CsumR::Cinr(b2)) => {
65                B::commutative(b1, b2);
66            },
67            _ => {},
68        }
69    }
70
71    proof fn associative(a: Self, b: Self, c: Self) {
72        match (a, b, c) {
73            (CsumR::Cinl(a1), CsumR::Cinl(a2), CsumR::Cinl(a3)) => {
74                A::associative(a1, a2, a3);
75            },
76            (CsumR::Cinr(b1), CsumR::Cinr(b2), CsumR::Cinr(b3)) => {
77                B::associative(b1, b2, b3);
78            },
79            _ => {},
80        }
81    }
82
83    proof fn op_unit(a: Self) {
84    }
85
86    proof fn unit_valid() {
87    }
88}
89
90} // verus!
vstd_extra/resource/pcm/csum.rs

vstd_extra/resource/pcm/
csum.rs
