vstd 0.0.0-2025-11-05-1950

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
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140

use super::prelude::*;

verus! {

pub trait ReadOperation: Sized {
    // tracked resource(s) passed to callback
    type Resource;

    // executable result returned from operation
    type ExecResult;

    spec fn requires(self, r: Self::Resource, e: Self::ExecResult) -> bool;

    // Optionally support peeking, which provides initial validation
    // before the operation is linearized.
    open spec fn peek_requires(self, r: Self::Resource) -> bool {
        true
    }

    open spec fn peek_ensures(self, r: Self::Resource) -> bool {
        true
    }
}

pub trait MutOperation: Sized {
    // tracked resource(s) passed to callback
    type Resource;

    // executable result returned from operation
    type ExecResult;

    // type of new value for the resource
    type NewState;

    spec fn requires(
        self,
        pre: Self::Resource,
        new_state: Self::NewState,
        e: Self::ExecResult,
    ) -> bool;

    spec fn ensures(
        self,
        pre: Self::Resource,
        post: Self::Resource,
        new_state: Self::NewState,
    ) -> bool;

    // Optionally support peeking, which provides initial validation
    // before the operation is linearized.
    open spec fn peek_requires(self, r: Self::Resource) -> bool {
        true
    }

    open spec fn peek_ensures(self, r: Self::Resource) -> bool {
        true
    }
}

pub trait ReadLinearizer<Op: ReadOperation>: Sized {
    type Completion;

    open spec fn namespaces(self) -> Set<int> {
        Set::empty()
    }

    open spec fn pre(self, op: Op) -> bool {
        true
    }

    open spec fn post(self, op: Op, r: Op::ExecResult, c: Self::Completion) -> bool {
        true
    }

    proof fn apply(
        tracked self,
        op: Op,
        tracked r: &Op::Resource,
        e: &Op::ExecResult,
    ) -> (tracked out: Self::Completion)
        requires
            self.pre(op),
            op.requires(*r, *e),
        ensures
            self.post(op, *e, out),
        opens_invariants self.namespaces()
    ;

    proof fn peek(tracked &self, op: Op, tracked r: &Op::Resource)
        requires
            self.pre(op),
            op.peek_requires(*r),
        ensures
            op.peek_ensures(*r),
        opens_invariants self.namespaces()
    ;
}

pub trait MutLinearizer<Op: MutOperation>: Sized {
    type Completion;

    open spec fn namespaces(self) -> Set<int> {
        Set::empty()
    }

    open spec fn pre(self, op: Op) -> bool {
        true
    }

    open spec fn post(self, op: Op, r: Op::ExecResult, c: Self::Completion) -> bool {
        true
    }

    proof fn apply(
        tracked self,
        op: Op,
        tracked r: &mut Op::Resource,
        new_state: Op::NewState,
        e: &Op::ExecResult,
    ) -> (tracked out: Self::Completion)
        requires
            self.pre(op),
            op.requires(*old(r), new_state, *e),
        ensures
            op.ensures(*old(r), *r, new_state),
            self.post(op, *e, out),
        opens_invariants self.namespaces()
    ;

    proof fn peek(tracked &self, op: Op, tracked r: &Op::Resource)
        requires
            self.pre(op),
            op.peek_requires(*r),
        ensures
            op.peek_ensures(*r),
        opens_invariants self.namespaces()
    ;
}

} // verus!