vstd 0.0.0-2026-06-14-0213

Verus Standard Library: Useful specifications and lemmas for verifying Rust code
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33

use super::super::prelude::*;
use super::algebra::ResourceAlgebra;

verus! {

pub enum ExclusiveRA<T> {
    Exclusive(T),
    Invalid,
}

impl<T> ResourceAlgebra for ExclusiveRA<T> {
    open spec fn valid(self) -> bool {
        match self {
            ExclusiveRA::Invalid => false,
            _ => true,
        }
    }

    open spec fn op(a: Self, b: Self) -> Self {
        ExclusiveRA::Invalid
    }

    proof fn associative(a: Self, b: Self, c: Self) {
    }

    proof fn commutative(a: Self, b: Self) {
    }

    proof fn valid_op(a: Self, b: Self) {
    }
}

} // verus!