vstd/resource/
product.rs

1use super::super::prelude::*;
2use super::algebra::ResourceAlgebra;
3use super::pcm::PCM;
4
5verus! {
6
7pub struct ProductRA<RA1: ResourceAlgebra, RA2: ResourceAlgebra> {
8    pub left: RA1,
9    pub right: RA2,
10}
11
12// Rust does not support variadic generics, so we define the product pairwise
13impl<RA1: ResourceAlgebra, RA2: ResourceAlgebra> ResourceAlgebra for ProductRA<RA1, RA2> {
14    open spec fn valid(self) -> bool {
15        self.left.valid() && self.right.valid()
16    }
17
18    open spec fn op(a: Self, b: Self) -> Self {
19        ProductRA { left: RA1::op(a.left, b.left), right: RA2::op(a.right, b.right) }
20    }
21
22    proof fn associative(a: Self, b: Self, c: Self) {
23        RA1::associative(a.left, b.left, c.left);
24        RA2::associative(a.right, b.right, c.right);
25    }
26
27    proof fn commutative(a: Self, b: Self) {
28        RA1::commutative(a.left, b.left);
29        RA2::commutative(a.right, b.right);
30    }
31
32    proof fn valid_op(a: Self, b: Self) {
33        RA1::valid_op(a.left, b.left);
34        RA2::valid_op(a.right, b.right);
35    }
36}
37
38impl<P1: PCM, P2: PCM> PCM for ProductRA<P1, P2> {
39    open spec fn unit() -> Self {
40        ProductRA { left: P1::unit(), right: P2::unit() }
41    }
42
43    proof fn op_unit(self) {
44        P1::op_unit(self.left);
45        P2::op_unit(self.right);
46    }
47
48    proof fn unit_valid() {
49        P1::unit_valid();
50        P2::unit_valid();
51    }
52}
53
54} // verus!
vstd/resource/product.rs

vstd/resource/
product.rs
