Skip to main content

vstd/resource/
exclusive.rs

1use super::super::prelude::*;
2use super::algebra::ResourceAlgebra;
3
4verus! {
5
6pub enum ExclusiveRA<T> {
7    Exclusive(T),
8    Invalid,
9}
10
11impl<T> ResourceAlgebra for ExclusiveRA<T> {
12    open spec fn valid(self) -> bool {
13        match self {
14            ExclusiveRA::Invalid => false,
15            _ => true,
16        }
17    }
18
19    open spec fn op(a: Self, b: Self) -> Self {
20        ExclusiveRA::Invalid
21    }
22
23    proof fn associative(a: Self, b: Self, c: Self) {
24    }
25
26    proof fn commutative(a: Self, b: Self) {
27    }
28
29    proof fn valid_op(a: Self, b: Self) {
30    }
31}
32
33} // verus!