vstd_extra/
rcu_objects.rs

1// SPDX-License-Identifier: MPL-2.0
2//! Allocation identity and ownership resources for RCU proofs.
3//!
4//! # Verified Properties
5//!
6//! Each registration receives a fresh allocation ID within its domain. Persistent
7//! block information preserves that ID across publications, including after the
8//! physical address is reused. A separate linear permission belongs to the same
9//! registration and will be consumed by the retirement protocol.
10//!
11//! Registration records identity only: neither block information nor a base
12//! retire permission grants access to the allocation or permission to reclaim it.
13//! A registered object can retain a client-defined linear resource, whose meaning
14//! remains the client's responsibility.
15use crate::ownership::Inv;
16use vstd::{
17    prelude::*,
18    resource::{
19        Loc,
20        map::{GhostMapAuth, GhostPersistentPointsTo, GhostPointsTo},
21    },
22};
23
24verus! {
25
26/// Authoritative allocation registry for one RCU protection domain.
27pub tracked struct RcuDomainAuth {
28    objects: GhostMapAuth<nat, usize>,
29    retire_perms: GhostMapAuth<nat, usize>,
30    ghost next_obj: nat,
31}
32
33impl Inv for RcuDomainAuth {
34    closed spec fn inv(self) -> bool {
35        &&& self.objects@ == self.retire_perms@
36        &&& forall|obj: nat| #[trigger] self.objects@.contains_key(obj) ==> obj < self.next_obj
37    }
38}
39
40impl RcuDomainAuth {
41    /// Stable identity of this protection domain.
42    pub closed spec fn id(self) -> Loc {
43        self.objects.id()
44    }
45
46    /// Registered allocation IDs and their physical addresses.
47    pub closed spec fn objects(self) -> Map<nat, usize> {
48        self.objects@
49    }
50
51    /// Fresh ID reserved for the next registration.
52    pub closed spec fn next_obj(self) -> nat {
53        self.next_obj
54    }
55
56    /// Resource registry that owns the unique base retire permissions.
57    pub closed spec fn retire_registry(self) -> Loc {
58        self.retire_perms.id()
59    }
60
61    /// Creates an empty RCU protection domain.
62    ///
63    /// # Postconditions
64    /// The invariant holds and the first registration receives ID zero.
65    pub proof fn tracked_new() -> (tracked res: Self)
66        ensures
67            res.inv(),
68            res.objects() == Map::<nat, usize>::empty(),
69            res.next_obj() == 0,
70    {
71        let tracked (objects, _) = GhostMapAuth::new(Map::empty());
72        let tracked (retire_perms, _) = GhostMapAuth::new(Map::empty());
73        RcuDomainAuth { objects, retire_perms, next_obj: 0 }
74    }
75
76    /// Registers a non-null pointer with a fresh allocation ID.
77    ///
78    /// # Preconditions
79    /// The domain invariant holds and the pointer is non-null. Registering an
80    /// address does not establish that it points to a live allocation.
81    ///
82    /// # Postconditions
83    /// Existing registrations are preserved. The returned persistent identity
84    /// and linear permission describe the same new registration.
85    pub proof fn tracked_register<T>(tracked &mut self, ptr: *mut T) -> (tracked res:
86        RcuRegistration<T>)
87        requires
88            old(self).inv(),
89            ptr.addr() != 0,
90        ensures
91            final(self).inv(),
92            final(self).id() == old(self).id(),
93            final(self).retire_registry() == old(self).retire_registry(),
94            final(self).next_obj() == old(self).next_obj() + 1,
95            final(self).objects() == old(self).objects().insert(old(self).next_obj(), ptr.addr()),
96            !old(self).objects().contains_key(res.0.obj()),
97            res.0.domain() == final(self).id(),
98            res.0.obj() == old(self).next_obj(),
99            res.0.ptr() == ptr,
100            res.0.addr() == ptr.addr(),
101            res.0.inv(),
102            res.1.domain() == res.0.domain(),
103            res.1.obj() == res.0.obj(),
104            res.1.ptr() == ptr,
105            res.1.inv(),
106            res.1.belongs_to(*final(self)),
107    {
108        let ghost obj = self.next_obj;
109        let tracked object = self.objects.insert(obj, ptr.addr());
110        let tracked info = object.persist();
111        let tracked perm = self.retire_perms.insert(obj, ptr.addr());
112        self.next_obj = self.next_obj + 1;
113
114        assert forall|registered: nat| #[trigger]
115            self.objects@.contains_key(registered) implies registered < self.next_obj by {
116            if registered != obj {
117                assert(old(self).objects().contains_key(registered));
118            }
119        };
120
121        (RcuBlockInfo { info, ptr }, RcuBaseRetirePerm { domain: self.id(), perm, ptr })
122    }
123
124    /// Agrees a persistent registration with its authoritative address entry.
125    ///
126    /// # Preconditions
127    /// The block information belongs to this protection domain.
128    ///
129    /// # Postconditions
130    /// The domain contains the recorded allocation ID and address.
131    pub proof fn lemma_block_info_agree<T>(tracked &self, tracked info: &RcuBlockInfo<T>)
132        requires
133            info.domain() == self.id(),
134        ensures
135            self.objects().contains_pair(info.obj(), info.addr()),
136    {
137        info.info.agree(&self.objects);
138    }
139}
140
141/// Persistent identity of one registered allocation, without physical ownership.
142#[verifier::reject_recursive_types(T)]
143pub tracked struct RcuBlockInfo<T> {
144    info: GhostPersistentPointsTo<nat, usize>,
145    ghost ptr: *mut T,
146}
147
148impl<T> Inv for RcuBlockInfo<T> {
149    closed spec fn inv(self) -> bool {
150        &&& self.addr() == self.ptr().addr()
151        &&& self.ptr().addr() != 0
152    }
153}
154
155impl<T> RcuBlockInfo<T> {
156    /// Protection domain in which the allocation was registered.
157    pub closed spec fn domain(self) -> Loc {
158        self.info.id()
159    }
160
161    /// Allocation ID, independent of address and publication timestamp.
162    pub closed spec fn obj(self) -> nat {
163        self.info.key()
164    }
165
166    /// Typed pointer supplied at registration.
167    pub closed spec fn ptr(self) -> *mut T {
168        self.ptr
169    }
170
171    /// Physical address recorded in the authoritative registry.
172    pub closed spec fn addr(self) -> usize {
173        self.info.value()
174    }
175
176    /// Exposes the address facts hidden by the registration invariant.
177    ///
178    /// # Preconditions
179    /// The block information satisfies its invariant.
180    ///
181    /// # Postconditions
182    /// Its recorded address equals the pointer address and is nonzero.
183    pub proof fn lemma_address(tracked &self)
184        requires
185            self.inv(),
186        ensures
187            self.addr() == self.ptr().addr(),
188            self.ptr().addr() != 0,
189    {
190    }
191
192    /// Duplicates persistent block information for another publication.
193    ///
194    /// # Postconditions
195    /// The duplicate describes exactly the same registration.
196    pub proof fn tracked_duplicate(tracked &self) -> (tracked res: Self)
197        ensures
198            res.domain() == self.domain(),
199            res.obj() == self.obj(),
200            res.ptr() == self.ptr(),
201            res.addr() == self.addr(),
202            res.inv() == self.inv(),
203    {
204        let tracked info = self.info.duplicate();
205        RcuBlockInfo { info, ptr: self.ptr }
206    }
207}
208
209/// Unique base permission retained until the allocation is retired.
210///
211/// This token supplies linear identity, not evidence of detachment or a grace
212/// period. It cannot justify reclaiming physical ownership by itself.
213#[verifier::reject_recursive_types(T)]
214pub tracked struct RcuBaseRetirePerm<T> {
215    ghost domain: Loc,
216    perm: GhostPointsTo<nat, usize>,
217    ghost ptr: *mut T,
218}
219
220impl<T> Inv for RcuBaseRetirePerm<T> {
221    closed spec fn inv(self) -> bool {
222        &&& self.addr() == self.ptr().addr()
223        &&& self.ptr().addr() != 0
224    }
225}
226
227impl<T> RcuBaseRetirePerm<T> {
228    /// Protection domain of the matching block information.
229    pub closed spec fn domain(self) -> Loc {
230        self.domain
231    }
232
233    /// Allocation ID for which this permission is unique.
234    pub closed spec fn obj(self) -> nat {
235        self.perm.key()
236    }
237
238    /// Typed pointer supplied at registration.
239    pub closed spec fn ptr(self) -> *mut T {
240        self.ptr
241    }
242
243    /// Physical address of the registered allocation.
244    pub closed spec fn addr(self) -> usize {
245        self.perm.value()
246    }
247
248    /// Binds the permission to both registries owned by the domain.
249    pub closed spec fn belongs_to(self, domain: RcuDomainAuth) -> bool {
250        &&& self.domain() == domain.id()
251        &&& self.perm.id() == domain.retire_registry()
252    }
253
254    /// Proves that two base retire permissions cannot name the same allocation.
255    ///
256    /// # Preconditions
257    /// Both permissions belong to the same domain.
258    ///
259    /// # Postconditions
260    /// Their allocation IDs differ and this permission is preserved.
261    pub proof fn lemma_distinct(tracked &mut self, tracked other: &Self, domain: RcuDomainAuth)
262        requires
263            old(self).belongs_to(domain),
264            other.belongs_to(domain),
265        ensures
266            final(self).domain() == old(self).domain(),
267            final(self).obj() == old(self).obj(),
268            final(self).ptr() == old(self).ptr(),
269            final(self).addr() == old(self).addr(),
270            final(self).inv() == old(self).inv(),
271            final(self).belongs_to(domain),
272            final(self).obj() != other.obj(),
273    {
274        self.perm.disjoint(&other.perm);
275    }
276}
277
278/// Persistent identity and linear base retire permission from one registration.
279pub type RcuRegistration<T> = (RcuBlockInfo<T>, RcuBaseRetirePerm<T>);
280
281/// Proves that address reuse creates a new ID while duplication preserves it.
282///
283/// # Preconditions
284/// The pointer has a nonzero address.
285///
286/// # Postconditions
287/// Two copies of the first registration agree, while a second registration at
288/// that same address has a different allocation ID in the same domain.
289pub proof fn lemma_registration_distinguishes_reused_address<T>(ptr: *mut T) -> (tracked res: (
290    RcuBlockInfo<T>,
291    RcuBlockInfo<T>,
292    RcuBlockInfo<T>,
293))
294    requires
295        ptr.addr() != 0,
296    ensures
297        res.0.domain() == res.1.domain(),
298        res.0.domain() == res.2.domain(),
299        res.0.obj() == res.1.obj(),
300        res.0.obj() < res.2.obj(),
301        res.0.addr() == res.1.addr() == res.2.addr() == ptr.addr(),
302{
303    let tracked mut domain = RcuDomainAuth::tracked_new();
304    let tracked (first, _) = domain.tracked_register(ptr);
305    let tracked history_copy = first.tracked_duplicate();
306    let tracked (second, _) = domain.tracked_register(ptr);
307    assert(first.domain() == history_copy.domain());
308    assert(first.domain() == second.domain());
309    assert(first.obj() == history_copy.obj());
310    assert(first.obj() < second.obj());
311    assert(first.addr() == history_copy.addr() == second.addr() == ptr.addr());
312    domain.lemma_block_info_agree(&history_copy);
313    assert(domain.objects().contains_pair(first.obj(), ptr.addr()));
314    (first, history_copy, second)
315}
316
317/// One allocation's registration paired with a linear client resource.
318#[verifier::reject_recursive_types(T)]
319pub tracked struct RcuOwnedObject<T, O> {
320    registration: RcuRegistration<T>,
321    ownership: O,
322}
323
324impl<T, O> Inv for RcuOwnedObject<T, O> {
325    open spec fn inv(self) -> bool {
326        &&& self.block_info().inv()
327        &&& self.retire_perm().inv()
328        &&& self.block_info().domain() == self.retire_perm().domain()
329        &&& self.block_info().obj() == self.retire_perm().obj()
330        &&& equal(self.block_info().ptr(), self.retire_perm().ptr())
331    }
332}
333
334impl<T, O> RcuOwnedObject<T, O> {
335    /// Persistent identity and unique base retire permission.
336    pub closed spec fn registration(self) -> RcuRegistration<T> {
337        self.registration
338    }
339
340    /// Persistent identity of the registered allocation.
341    pub open spec fn block_info(self) -> RcuBlockInfo<T> {
342        self.registration().0
343    }
344
345    /// Unique base retire permission for the registered allocation.
346    pub open spec fn retire_perm(self) -> RcuBaseRetirePerm<T> {
347        self.registration().1
348    }
349
350    /// Client resource associated with this registration.
351    pub closed spec fn ownership(self) -> O {
352        self.ownership
353    }
354
355    /// Pairs a consistent registration with a client resource without copying either.
356    pub proof fn tracked_new(
357        tracked registration: RcuRegistration<T>,
358        tracked ownership: O,
359    ) -> (tracked res: Self)
360        requires
361            registration.0.inv(),
362            registration.1.inv(),
363            registration.0.domain() == registration.1.domain(),
364            registration.0.obj() == registration.1.obj(),
365            equal(registration.0.ptr(), registration.1.ptr()),
366        ensures
367            res.inv(),
368            res.registration() == registration,
369            res.ownership() == ownership,
370    {
371        Self { registration, ownership }
372    }
373
374    /// Consumes the wrapper and returns its unchanged registration and client resource.
375    pub proof fn tracked_into_parts(tracked self) -> tracked (RcuRegistration<T>, O)
376        returns
377            (self.registration(), self.ownership()),
378    {
379        (self.registration, self.ownership)
380    }
381}
382
383} // verus!
vstd_extra/rcu_objects.rs

vstd_extra/
rcu_objects.rs
