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::*;
11
12use vstd_extra::cast_ptr::Repr;
13use vstd_extra::drop_tracking::*;
14
15use crate::mm::frame::Frame;
16use crate::mm::page_table::{PageTableConfig, PageTableGuard, PageTablePageMeta};
17use crate::specs::mm::frame::meta_owners::{MetaSlotStorage, StoredPageTablePageMeta};
18
19verus! {
20
21pub tracked struct Guards<'rcu> {
22    /// The set of node addresses that are currently guarded (locked).
23    pub ghost guards: Set<usize>,
24    pub _phantom: PhantomData<&'rcu ()>,
25}
26
27impl<'rcu> Guards<'rcu> {
28    pub open spec fn locked(self, addr: usize) -> bool {
29        self.guards.contains(addr)
30    }
31
32    pub open spec fn unlocked(self, addr: usize) -> bool {
33        !self.guards.contains(addr)
34    }
35
36    pub open spec fn lock_held(self, addr: usize) -> bool {
37        self.guards.contains(addr)
38    }
39}
40
41impl<'rcu, C: PageTableConfig> TrackDrop for PageTableGuard<'rcu, C> {
42    type State = Guards<'rcu>;
43
44    /// The node address whose lock this guard holds. The token
45    /// thus identifies *which* guard it tracks; `drop_requires`'s key
46    /// match prevents a guard's obligation from being used to drop a
47    /// different guard. The real lock-set ledger is `Guards::guards`;
48    /// this trait's discipline lifts the existing state-side discipline
49    /// onto the obligation token by carrying the locked address.
50    type Key = usize;
51
52    open spec fn key(self) -> Self::Key {
53        self.inner.inner@.ptr.addr()
54    }
55
56    open spec fn constructor_requires(self, s: Self::State) -> bool {
57        s.lock_held(self.inner.inner@.ptr.addr())
58    }
59
60    open spec fn constructor_ensures(
61        self,
62        s0: Self::State,
63        s1: Self::State,
64        obl_key: Self::Key,
65    ) -> bool {
66        &&& s1.guards == s0.guards.remove(self.inner.inner@.ptr.addr())
67        &&& obl_key == self.inner.inner@.ptr.addr()
68    }
69
70    proof fn constructor_spec(self, tracked s: &mut Self::State) -> (tracked obl: DropObligation<
71        Self::Key,
72    >) {
73        s.guards = s.guards.remove(self.inner.inner@.ptr.addr());
74        DropObligation::tracked_mint(self.inner.inner@.ptr.addr())
75    }
76
77    open spec fn drop_requires(self, s: Self::State) -> bool {
78        s.unlocked(self.inner.inner@.ptr.addr())
79    }
80
81    open spec fn drop_ensures(self, s0: Self::State, s1: Self::State, obl_key: Self::Key) -> bool {
82        s1.guards == s0.guards.insert(self.inner.inner@.ptr.addr())
83    }
84
85    open spec fn consume_requires(self, s: Self::State, obl_key: Self::Key) -> bool {
86        // The token must identify this guard's locked address — prevents
87        // a token forged for a different guard from discharging this one.
88        obl_key == self.inner.inner@.ptr.addr()
89    }
90
91    open spec fn consume_ensures(
92        self,
93        s0: Self::State,
94        s1: Self::State,
95        obl_key: Self::Key,
96    ) -> bool {
97        s1.guards == s0.guards.remove(self.inner.inner@.ptr.addr())
98    }
99
100    proof fn consume_obligation(
101        self,
102        tracked s: &mut Self::State,
103        tracked obl: DropObligation<Self::Key>,
104    ) {
105        // Release this guard's lock from the held-lock ledger.
106        s.guards = s.guards.remove(self.inner.inner@.ptr.addr());
107    }
108}
109
110impl<C: PageTableConfig> PageTablePageMeta<C> {
111    pub open spec fn into_spec(self) -> StoredPageTablePageMeta {
112        StoredPageTablePageMeta {
113            nr_children: self.nr_children,
114            stray: self.stray,
115            level: self.level,
116            lock: self.lock,
117        }
118    }
119
120    #[verifier::when_used_as_spec(into_spec)]
121    pub fn into(self) -> (res: StoredPageTablePageMeta)
122        ensures
123            res == self.into_spec(),
124    {
125        StoredPageTablePageMeta {
126            nr_children: self.nr_children,
127            stray: self.stray,
128            level: self.level,
129            lock: self.lock,
130        }
131    }
132}
133
134impl StoredPageTablePageMeta {
135    pub open spec fn into_spec<C: PageTableConfig>(self) -> PageTablePageMeta<C> {
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    #[verifier::when_used_as_spec(into_spec)]
146    pub fn into<C: PageTableConfig>(self) -> (res: PageTablePageMeta<C>)
147        ensures
148            res == self.into_spec::<C>(),
149    {
150        PageTablePageMeta::<C> {
151            nr_children: self.nr_children,
152            stray: self.stray,
153            level: self.level,
154            lock: self.lock,
155            _phantom: PhantomData,
156        }
157    }
158}
159
160pub uninterp spec fn drop_tree_spec<C: PageTableConfig>(
161    _page: Frame<PageTablePageMeta<C>>,
162) -> Frame<PageTablePageMeta<C>>;
163
164impl<C: PageTableConfig> Repr<MetaSlotStorage> for PageTablePageMeta<C> {
165    type Perm = ();
166
167    open spec fn wf(r: MetaSlotStorage, perm: ()) -> bool {
168        matches!(r, MetaSlotStorage::PTNode(_))
169    }
170
171    open spec fn to_repr_spec(self, perm: ()) -> (MetaSlotStorage, ()) {
172        (MetaSlotStorage::PTNode(self.into_spec()), ())
173    }
174
175    #[verifier::external_body]
176    fn to_repr(self, Tracked(perm): Tracked<&mut ()>) -> MetaSlotStorage {
177        unimplemented!()
178    }
179
180    open spec fn from_repr_spec(r: MetaSlotStorage, perm: ()) -> Self {
181        match r {
182            MetaSlotStorage::PTNode(node) => node.into_spec::<C>(),
183            _ => arbitrary(),
184        }
185    }
186
187    #[verifier::external_body]
188    fn from_repr(r: MetaSlotStorage, Tracked(perm): Tracked<&()>) -> Self {
189        unimplemented!()
190    }
191
192    #[verifier::external_body]
193    fn from_borrowed<'a>(r: &'a MetaSlotStorage, Tracked(perm): Tracked<&'a ()>) -> &'a Self {
194        unimplemented!()
195    }
196
197    proof fn from_to_repr(self, perm: ()) {
198        assert(self.to_repr_spec(perm) == (MetaSlotStorage::PTNode(self.into_spec()), ()));
199        assert(StoredPageTablePageMeta::into_spec::<C>(self.into_spec()) == self);
200    }
201
202    proof fn to_from_repr(r: MetaSlotStorage, perm: ()) {
203        match r {
204            MetaSlotStorage::PTNode(node) => {
205                assert(Self::from_repr_spec(r, perm) == node.into_spec::<C>());
206                assert(Self::from_repr_spec(r, perm).to_repr_spec(perm) == (
207                    MetaSlotStorage::PTNode(node),
208                    (),
209                ));
210            },
211            _ => {
212                assert(false);
213            },
214        }
215    }
216
217    proof fn to_repr_wf(self, perm: ()) {
218        assert(self.to_repr_spec(perm).0 is PTNode);
219    }
220}
221
222} // verus!
ostd/specs/mm/page_table/node/mod.rs

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