vstd/
logatom.rs

1use super::prelude::*;
2
3verus! {
4
5pub trait ReadOperation: Sized {
6    // tracked resource(s) passed to callback
7    type Resource;
8
9    // executable result returned from operation
10    type ExecResult;
11
12    spec fn requires(self, r: Self::Resource, e: Self::ExecResult) -> bool;
13
14    // Optionally support peeking, which provides initial validation
15    // before the operation is linearized.
16    open spec fn peek_requires(self, r: Self::Resource) -> bool {
17        true
18    }
19
20    open spec fn peek_ensures(self, r: Self::Resource) -> bool {
21        true
22    }
23}
24
25pub trait MutOperation: Sized {
26    // tracked resource(s) passed to callback
27    type Resource;
28
29    // executable result returned from operation
30    type ExecResult;
31
32    // type of new value for the resource
33    type NewState;
34
35    spec fn requires(
36        self,
37        pre: Self::Resource,
38        new_state: Self::NewState,
39        e: Self::ExecResult,
40    ) -> bool;
41
42    spec fn ensures(
43        self,
44        pre: Self::Resource,
45        post: Self::Resource,
46        new_state: Self::NewState,
47    ) -> bool;
48
49    // Optionally support peeking, which provides initial validation
50    // before the operation is linearized.
51    open spec fn peek_requires(self, r: Self::Resource) -> bool {
52        true
53    }
54
55    open spec fn peek_ensures(self, r: Self::Resource) -> bool {
56        true
57    }
58}
59
60pub trait ReadLinearizer<Op: ReadOperation>: Sized {
61    type Completion;
62
63    open spec fn namespaces(self) -> Set<int> {
64        Set::empty()
65    }
66
67    open spec fn pre(self, op: Op) -> bool {
68        true
69    }
70
71    open spec fn post(self, op: Op, r: Op::ExecResult, c: Self::Completion) -> bool {
72        true
73    }
74
75    proof fn apply(
76        tracked self,
77        op: Op,
78        tracked r: &Op::Resource,
79        e: &Op::ExecResult,
80    ) -> (tracked out: Self::Completion)
81        requires
82            self.pre(op),
83            op.requires(*r, *e),
84        ensures
85            self.post(op, *e, out),
86        opens_invariants self.namespaces()
87    ;
88
89    proof fn peek(tracked &self, op: Op, tracked r: &Op::Resource)
90        requires
91            self.pre(op),
92            op.peek_requires(*r),
93        ensures
94            op.peek_ensures(*r),
95        opens_invariants self.namespaces()
96    ;
97}
98
99pub trait MutLinearizer<Op: MutOperation>: Sized {
100    type Completion;
101
102    open spec fn namespaces(self) -> Set<int> {
103        Set::empty()
104    }
105
106    open spec fn pre(self, op: Op) -> bool {
107        true
108    }
109
110    open spec fn post(self, op: Op, r: Op::ExecResult, c: Self::Completion) -> bool {
111        true
112    }
113
114    proof fn apply(
115        tracked self,
116        op: Op,
117        tracked r: &mut Op::Resource,
118        new_state: Op::NewState,
119        e: &Op::ExecResult,
120    ) -> (tracked out: Self::Completion)
121        requires
122            self.pre(op),
123            op.requires(*old(r), new_state, *e),
124        ensures
125            op.ensures(*old(r), *r, new_state),
126            self.post(op, *e, out),
127        opens_invariants self.namespaces()
128    ;
129
130    proof fn peek(tracked &self, op: Op, tracked r: &Op::Resource)
131        requires
132            self.pre(op),
133            op.peek_requires(*r),
134        ensures
135            op.peek_ensures(*r),
136        opens_invariants self.namespaces()
137    ;
138}
139
140} // verus!
vstd/logatom.rs

vstd/
logatom.rs
