ostd/specs/mm/page_table/node/
mod.rs

1pub mod entry_owners;
2pub mod entry_view;
3pub mod owners;
4pub mod page_table_node_specs;
5
6pub use entry_owners::*;
7pub use entry_view::*;
8pub use owners::*;
9pub use page_table_node_specs::*;
10
11use vstd::prelude::*;
12use vstd::simple_pptr::*;
13
14use vstd_extra::undroppable::*;
15
16use crate::mm::page_table::{PageTableConfig, PageTableGuard};
17
18verus! {
19
20pub type GuardPerm<'rcu, C: PageTableConfig> = PointsTo<PageTableGuard<'rcu, C>>;
21
22pub tracked struct Guards<'rcu, C: PageTableConfig> {
23    pub guards: Map<usize, Option<GuardPerm<'rcu, C>>>,
24}
25
26impl<'rcu, C: PageTableConfig> Guards<'rcu, C> {
27    pub open spec fn locked(self, addr: usize) -> bool {
28        self.guards.contains_key(addr)
29    }
30
31    pub open spec fn unlocked(self, addr: usize) -> bool {
32        !self.guards.contains_key(addr)
33    }
34
35    pub open spec fn lock_held(self, addr: usize) -> bool {
36        self.guards.contains_key(addr) && self.guards[addr] is None
37    }
38
39    pub proof fn take(tracked &mut self, addr: usize) -> (tracked guard: GuardPerm<'rcu, C>)
40        requires
41            old(self).locked(addr),
42            old(self).guards[addr] is Some,
43        ensures
44            self.lock_held(addr),
45            guard == old(self).guards[addr].unwrap(),
46    {
47        let tracked guard = self.guards.tracked_remove(addr).tracked_unwrap();
48        self.guards.tracked_insert(addr, None);
49        guard
50    }
51
52    pub proof fn put(tracked &mut self, addr: usize, tracked guard: GuardPerm<'rcu, C>)
53        requires
54            old(self).lock_held(addr),
55        ensures
56            self.locked(addr),
57            self.guards[addr] == Some(guard),
58    {
59        let _ = self.guards.tracked_remove(addr);
60        self.guards.tracked_insert(addr, Some(guard));
61    }
62}
63
64impl<'rcu, C: PageTableConfig> Undroppable for PageTableGuard<'rcu, C> {
65    type State = Guards<'rcu, C>;
66
67    open spec fn constructor_requires(self, s: Self::State) -> bool {
68        s.lock_held(self.inner.inner@.ptr.addr())
69    }
70
71    open spec fn constructor_ensures(self, s0: Self::State, s1: Self::State) -> bool {
72        s1.guards == s0.guards.remove(self.inner.inner@.ptr.addr())
73    }
74
75    proof fn constructor_spec(self, tracked s: &mut Self::State)
76    {
77        s.guards.tracked_remove(self.inner.inner@.ptr.addr());
78    }
79}
80
81} // verus!
ostd/specs/mm/page_table/node/mod.rs

ostd/specs/mm/page_table/node/
mod.rs
