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

1pub mod entry_owners;
2pub mod entry_view;
3pub mod owners;
4
5pub use entry_owners::*;
6pub use entry_view::*;
7pub use owners::*;
8
9use core::marker::PhantomData;
10use vstd::prelude::*;
11use vstd::simple_pptr::*;
12
13use vstd_extra::cast_ptr::Repr;
14use vstd_extra::drop_tracking::*;
15
16use crate::mm::frame::Frame;
17use crate::mm::page_table::{PageTableConfig, PageTableGuard, PageTablePageMeta};
18use crate::specs::mm::frame::meta_owners::{MetaSlotStorage, StoredPageTablePageMeta};
19
20verus! {
21
22pub type GuardPerm<'rcu, C: PageTableConfig> = PointsTo<PageTableGuard<'rcu, C>>;
23
24pub tracked struct Guards<'rcu, C: PageTableConfig> {
25    pub guards: Map<usize, Option<GuardPerm<'rcu, C>>>,
26}
27
28impl<'rcu, C: PageTableConfig> Guards<'rcu, C> {
29    pub open spec fn locked(self, addr: usize) -> bool {
30        self.guards.contains_key(addr)
31    }
32
33    pub open spec fn unlocked(self, addr: usize) -> bool {
34        !self.guards.contains_key(addr)
35    }
36
37    pub open spec fn lock_held(self, addr: usize) -> bool {
38        self.guards.contains_key(addr) && self.guards[addr] is None
39    }
40
41    pub proof fn take(tracked &mut self, addr: usize) -> (tracked guard: GuardPerm<'rcu, C>)
42        requires
43            old(self).locked(addr),
44            old(self).guards[addr] is Some,
45        ensures
46            self.lock_held(addr),
47            guard == old(self).guards[addr].unwrap(),
48    {
49        let tracked guard = self.guards.tracked_remove(addr).tracked_unwrap();
50        self.guards.tracked_insert(addr, None);
51        guard
52    }
53
54    pub proof fn put(tracked &mut self, addr: usize, tracked guard: GuardPerm<'rcu, C>)
55        requires
56            old(self).lock_held(addr),
57        ensures
58            self.locked(addr),
59            self.guards[addr] == Some(guard),
60    {
61        let _ = self.guards.tracked_remove(addr);
62        self.guards.tracked_insert(addr, Some(guard));
63    }
64}
65
66impl<'rcu, C: PageTableConfig> TrackDrop for PageTableGuard<'rcu, C> {
67    type State = Guards<'rcu, C>;
68
69    open spec fn constructor_requires(self, s: Self::State) -> bool {
70        s.lock_held(self.inner.inner@.ptr.addr())
71    }
72
73    open spec fn constructor_ensures(self, s0: Self::State, s1: Self::State) -> bool {
74        s1.guards == s0.guards.remove(self.inner.inner@.ptr.addr())
75    }
76
77    proof fn constructor_spec(self, tracked s: &mut Self::State)
78    {
79        s.guards.tracked_remove(self.inner.inner@.ptr.addr());
80    }
81
82    open spec fn drop_requires(self, s: Self::State) -> bool {
83        s.unlocked(self.inner.inner@.ptr.addr())
84    }
85
86    open spec fn drop_ensures(self, s0: Self::State, s1: Self::State) -> bool {
87        s1.guards == s0.guards.insert(self.inner.inner@.ptr.addr(), None)
88    }
89
90    proof fn drop_spec(self, tracked s: &mut Self::State)
91    {
92        s.guards.tracked_insert(self.inner.inner@.ptr.addr(), None);
93    }
94}
95
96impl<C: PageTableConfig> PageTablePageMeta<C> {
97    pub open spec fn into_spec(self) -> StoredPageTablePageMeta {
98        StoredPageTablePageMeta {
99            nr_children: self.nr_children,
100            stray: self.stray,
101            level: self.level,
102            lock: self.lock,
103        }
104    }
105
106    #[verifier::when_used_as_spec(into_spec)]
107    pub fn into(self) -> (res: StoredPageTablePageMeta)
108        ensures
109            res == self.into_spec(),
110    {
111        StoredPageTablePageMeta {
112            nr_children: self.nr_children,
113            stray: self.stray,
114            level: self.level,
115            lock: self.lock,
116        }
117    }
118}
119
120impl StoredPageTablePageMeta {
121    pub open spec fn into_spec<C: PageTableConfig>(self) -> PageTablePageMeta<C> {
122        PageTablePageMeta::<C> {
123            nr_children: self.nr_children,
124            stray: self.stray,
125            level: self.level,
126            lock: self.lock,
127            _phantom: PhantomData,
128        }
129    }
130
131    #[verifier::when_used_as_spec(into_spec)]
132    pub fn into<C: PageTableConfig>(self) -> (res: PageTablePageMeta<C>)
133        ensures
134            res == self.into_spec::<C>(),
135    {
136        PageTablePageMeta::<C> {
137            nr_children: self.nr_children,
138            stray: self.stray,
139            level: self.level,
140            lock: self.lock,
141            _phantom: PhantomData,
142        }
143    }
144}
145
146pub uninterp spec fn drop_tree_spec<C: PageTableConfig>(_page: Frame<PageTablePageMeta<C>>) -> Frame<PageTablePageMeta<C>>;
147
148impl<C: PageTableConfig> Repr<MetaSlotStorage> for PageTablePageMeta<C> {
149    type Perm = ();
150
151    uninterp spec fn wf(r: MetaSlotStorage, perm: ()) -> bool;
152
153    uninterp spec fn to_repr_spec(self, perm: ()) -> (MetaSlotStorage, ());
154
155    #[verifier::external_body]
156    fn to_repr(self, Tracked(perm): Tracked<&mut ()>) -> MetaSlotStorage {
157        unimplemented!()
158    }
159
160    uninterp spec fn from_repr_spec(r: MetaSlotStorage, perm: ()) -> Self;
161
162    #[verifier::external_body]
163    fn from_repr(r: MetaSlotStorage, Tracked(perm): Tracked<&()>) -> Self {
164        unimplemented!()
165    }
166
167    #[verifier::external_body]
168    fn from_borrowed<'a>(r: &'a MetaSlotStorage, Tracked(perm): Tracked<&'a ()>) -> &'a Self {
169        unimplemented!()
170    }
171
172    proof fn from_to_repr(self, perm: ()) {
173        admit()
174    }
175
176    proof fn to_from_repr(r: MetaSlotStorage, perm: ()) {
177        admit()
178    }
179
180    proof fn to_repr_wf(self, perm: ()) {
181        admit()
182    }
183}
184
185} // verus!
ostd/specs/mm/page_table/node/mod.rs

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