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

vstd_extra/
rcu_objects.rs
