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
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55

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

verus! {

pub enum SumRA<RA1: ResourceAlgebra, RA2: ResourceAlgebra> {
    Left(RA1),
    Right(RA2),
    Invalid,
}

// Rust does not support variadic generics, so we define the sum pairwise
impl<RA1: ResourceAlgebra, RA2: ResourceAlgebra> ResourceAlgebra for SumRA<RA1, RA2> {
    open spec fn valid(self) -> bool {
        match self {
            SumRA::Left(l) => l.valid(),
            SumRA::Right(r) => r.valid(),
            SumRA::Invalid => false,
        }
    }

    open spec fn op(a: Self, b: Self) -> Self {
        match (a, b) {
            (SumRA::Left(la), SumRA::Left(lb)) => SumRA::Left(RA1::op(la, lb)),
            (SumRA::Right(ra), SumRA::Right(rb)) => SumRA::Right(RA2::op(ra, rb)),
            _ => SumRA::Invalid,
        }
    }

    proof fn associative(a: Self, b: Self, c: Self) {
        match (a, b, c) {
            (SumRA::Left(a), SumRA::Left(b), SumRA::Left(c)) => RA1::associative(a, b, c),
            (SumRA::Right(a), SumRA::Right(b), SumRA::Right(c)) => RA2::associative(a, b, c),
            (_, _, _) => {},
        }
    }

    proof fn commutative(a: Self, b: Self) {
        match (a, b) {
            (SumRA::Left(a), SumRA::Left(b)) => RA1::commutative(a, b),
            (SumRA::Right(a), SumRA::Right(b)) => RA2::commutative(a, b),
            (_, _) => {},
        }
    }

    proof fn valid_op(a: Self, b: Self) {
        match (a, b) {
            (SumRA::Left(a), SumRA::Left(b)) => RA1::valid_op(a, b),
            (SumRA::Right(a), SumRA::Right(b)) => RA2::valid_op(a, b),
            (_, _) => {},
        }
    }
}

} // verus!