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
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99

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

verus! {

/// The preorder relation.
/// `incl(a, b)` (or a ≼ b) means that there is some `c` such that `a · c == b`
pub open spec fn incl<RA: ResourceAlgebra>(a: RA, b: RA) -> bool {
    exists|c| RA::op(a, c) == b
}

pub open spec fn conjunct_shared<RA: ResourceAlgebra>(a: RA, b: RA, c: RA) -> bool {
    forall|p: RA| p.valid() && incl(a, p) && incl(b, p) ==> #[trigger] incl(c, p)
}

/// A frame preserving update is an update of a value from `a --> b` such that every value `c`
/// that could compose with `a` (also called the frame) can still compose with `b`.
pub open spec fn frame_preserving_update<P: PCM>(a: P, b: P) -> bool {
    forall|c| #![trigger P::op(a, c), P::op(b, c)] P::op(a, c).valid() ==> P::op(b, c).valid()
}

/// A nondeterministic version of a [`frame_preserving_update`].
pub open spec fn frame_preserving_update_nondeterministic<P: PCM>(a: P, bs: ISet<P>) -> bool {
    forall|c|
        #![trigger P::op(a, c)]
        P::op(a, c).valid() ==> exists|b| #[trigger] bs.contains(b) && P::op(b, c).valid()
}

/// A frame preserving update with support for resource algebras.
/// See [`frame_preserving_update`] for more details.
/// The difference lies in the fact that for [`PCM`]s there is always a unit
///
pub open spec fn frame_preserving_update_opt<RA: ResourceAlgebra>(a: RA, b: RA) -> bool {
    forall|c|
        #![trigger Option::<RA>::op(Some(a), c), Option::<RA>::op(Some(b), c)]
        Option::<RA>::op(Some(a), c).valid() ==> Option::<RA>::op(Some(b), c).valid()
}

/// A nondeterministic version of a [`frame_preserving_update_opt`].
pub open spec fn frame_preserving_update_nondeterministic_opt<RA: ResourceAlgebra>(
    a: RA,
    bs: ISet<RA>,
) -> bool {
    forall|c|
        #![trigger Option::<RA>::op(Some(a), c)]
        Option::<RA>::op(Some(a), c).valid() ==> exists|b| #[trigger]
            bs.contains(b) && Option::<RA>::op(Some(b), c).valid()
}

/// The set of values such that can be created by composing an element of `s` with `t`.
pub open spec fn set_op<RA: ResourceAlgebra>(s: ISet<RA>, t: RA) -> ISet<RA> {
    ISet::new(|v| exists|q| s.contains(q) && v == RA::op(q, t))
}

pub proof fn lemma_incl_transitive<RA: ResourceAlgebra>(a: RA, b: RA, c: RA)
    requires
        incl(a, b),
        incl(b, c),
    ensures
        incl(a, c),
{
    let ax = choose|ax| RA::op(a, ax) == b;
    let bx = choose|bx| RA::op(b, bx) == c;
    assert(RA::op(RA::op(a, ax), bx) == c);
    RA::associative(a, ax, bx);
    assert(RA::op(a, RA::op(ax, bx)) == c);
}

pub proof fn lemma_frame_preserving_opt<RA: ResourceAlgebra>(a: RA, b: RA)
    requires
        frame_preserving_update_opt::<RA>(a, b),
    ensures
        frame_preserving_update::<Option<RA>>(Some(a), Some(b)),
{
}

pub proof fn lemma_frame_preserving_update_nondeterministic_opt<RA: ResourceAlgebra>(
    a: RA,
    bs: ISet<RA>,
)
    requires
        frame_preserving_update_nondeterministic_opt::<RA>(a, bs),
    ensures
        frame_preserving_update_nondeterministic::<Option<RA>>(Some(a), bs.map(|b| Some(b))),
{
    broadcast use super::super::iset::group_iset_lemmas;

    let bs_mapped = bs.map(|b| Some(b));
    assert forall|c|
        #![trigger Option::<RA>::op(Some(a), c)]
        Option::<RA>::op(Some(a), c).valid() implies exists|b| #[trigger]
        bs_mapped.contains(b) && Option::<RA>::op(b, c).valid() by {
        let b = choose|b| #[trigger] bs.contains(b) && Option::<RA>::op(Some(b), c).valid();
        assert(bs_mapped.contains(Some(b)));
    }
}

} // verus!