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
56
57
58
59
60
61

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

verus! {

/// The Agreement resource algebra
///
/// This resource algebra allows one to express that multiple parties can _agree_ on a chosen value
/// This is mainly useful to show that if two resources are `Agree` then they must point to the
/// same value (see [`lemma_agree`]):
/// ```
pub enum AgreementRA<T> {
    Agree(T),
    Invalid,
}

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

    open spec fn op(a: Self, b: Self) -> Self {
        match (a, b) {
            (AgreementRA::Agree(a), AgreementRA::Agree(b)) if a == b => AgreementRA::Agree(a),
            _ => AgreementRA::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) {
    }
}

impl<T> AgreementRA<T> {
    pub open spec fn view(self) -> T {
        self->Agree_0
    }
}

pub proof fn lemma_agree<T>(
    tracked a: &Resource<AgreementRA<T>>,
    tracked b: &Resource<AgreementRA<T>>,
)
    requires
        a.loc() == b.loc(),
    ensures
        a.value()@ == b.value()@,
{
    a.join_shared(b).validate();
}

} // verus!