vstd_extra/resource/storage_protocol/
hybrid_product.rs

1//! Product of a PCM and a storage-protocol resource algebra.
2use core::marker::PhantomData;
3use vstd::pcm::PCM;
4use vstd::prelude::*;
5use vstd::storage_protocol::*;
6
7verus! {
8
9/// The hybrid product of a PCM and a storage-protocol resource algebra.
10pub ghost struct HybridProduct<P: PCM, S: Protocol<K, V>, K, V> {
11    pub pcm: P,
12    pub protocol: S,
13    /// A Rust compiler restriction.
14    pub _phantom: PhantomData<(K, V)>,
15}
16
17impl<P, S, K, V> Protocol<K, V> for HybridProduct<P, S, K, V> where P: PCM, S: Protocol<K, V> {
18    open spec fn op(self, other: Self) -> Self {
19        HybridProduct {
20            pcm: self.pcm.op(other.pcm),
21            protocol: self.protocol.op(other.protocol),
22            _phantom: PhantomData,
23        }
24    }
25
26    open spec fn rel(self, s: Map<K, V>) -> bool {
27        self.protocol.rel(s)
28    }
29
30    open spec fn unit() -> Self {
31        HybridProduct { pcm: P::unit(), protocol: S::unit(), _phantom: PhantomData }
32    }
33
34    proof fn commutative(a: Self, b: Self) {
35        P::commutative(a.pcm, b.pcm);
36        S::commutative(a.protocol, b.protocol);
37    }
38
39    proof fn associative(a: Self, b: Self, c: Self) {
40        P::associative(a.pcm, b.pcm, c.pcm);
41        S::associative(a.protocol, b.protocol, c.protocol);
42    }
43
44    proof fn op_unit(a: Self) {
45        P::op_unit(a.pcm);
46        S::op_unit(a.protocol);
47    }
48}
49
50impl<P, S, K, V> HybridProduct<P, S, K, V> where P: PCM, S: Protocol<K, V> {
51    pub open spec fn pcm(self) -> P {
52        self.pcm
53    }
54
55    pub open spec fn protocol(self) -> S {
56        self.protocol
57    }
58}
59
60} // verus!
vstd_extra/resource/storage_protocol/hybrid_product.rs

vstd_extra/resource/storage_protocol/
hybrid_product.rs
