vstd_extra/resource/storage/
hybrid_product.rs

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

vstd_extra/resource/storage/
hybrid_product.rs
