vstd/resource/
sum.rs

1use super::super::prelude::*;
2use super::algebra::ResourceAlgebra;
3
4verus! {
5
6pub enum SumRA<RA1: ResourceAlgebra, RA2: ResourceAlgebra> {
7    Left(RA1),
8    Right(RA2),
9    Invalid,
10}
11
12// Rust does not support variadic generics, so we define the sum pairwise
13impl<RA1: ResourceAlgebra, RA2: ResourceAlgebra> ResourceAlgebra for SumRA<RA1, RA2> {
14    open spec fn valid(self) -> bool {
15        match self {
16            SumRA::Left(l) => l.valid(),
17            SumRA::Right(r) => r.valid(),
18            SumRA::Invalid => false,
19        }
20    }
21
22    open spec fn op(a: Self, b: Self) -> Self {
23        match (a, b) {
24            (SumRA::Left(la), SumRA::Left(lb)) => SumRA::Left(RA1::op(la, lb)),
25            (SumRA::Right(ra), SumRA::Right(rb)) => SumRA::Right(RA2::op(ra, rb)),
26            _ => SumRA::Invalid,
27        }
28    }
29
30    proof fn associative(a: Self, b: Self, c: Self) {
31        match (a, b, c) {
32            (SumRA::Left(a), SumRA::Left(b), SumRA::Left(c)) => RA1::associative(a, b, c),
33            (SumRA::Right(a), SumRA::Right(b), SumRA::Right(c)) => RA2::associative(a, b, c),
34            (_, _, _) => {},
35        }
36    }
37
38    proof fn commutative(a: Self, b: Self) {
39        match (a, b) {
40            (SumRA::Left(a), SumRA::Left(b)) => RA1::commutative(a, b),
41            (SumRA::Right(a), SumRA::Right(b)) => RA2::commutative(a, b),
42            (_, _) => {},
43        }
44    }
45
46    proof fn valid_op(a: Self, b: Self) {
47        match (a, b) {
48            (SumRA::Left(a), SumRA::Left(b)) => RA1::valid_op(a, b),
49            (SumRA::Right(a), SumRA::Right(b)) => RA2::valid_op(a, b),
50            (_, _) => {},
51        }
52    }
53}
54
55} // verus!
vstd/resource/sum.rs

vstd/resource/
sum.rs
