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

1pub mod entry_owners;
2pub mod entry_view;
3pub mod owners;
4
5use vstd::prelude::*;
6use vstd_extra::{cast_ptr::Repr, drop_tracking::*};
7
8use crate::specs::mm::frame::meta_owners::{MetaSlotStorage, StoredPageTablePageMeta};
9
10use crate::mm::{
11    frame::Frame,
12    page_table::{PageTableConfig, PageTableGuard, PageTablePageMeta},
13};
14use core::marker::PhantomData;
15pub use entry_owners::*;
16pub use entry_view::*;
17pub use owners::*;
18
19verus! {
20
21pub tracked struct Guards {
22    /// The set of node addresses that are currently guarded (locked).
23    pub ghost guards: Set<usize>,
24}
25
26impl Guards {
27    pub open spec fn unlocked(self, addr: usize) -> bool {
28        !self.guards.contains(addr)
29    }
30
31    pub open spec fn lock_held(self, addr: usize) -> bool {
32        self.guards.contains(addr)
33    }
34}
35
36impl<'rcu, C: PageTableConfig> TrackDrop for PageTableGuard<'rcu, C> {
37    type State = Guards;
38
39    /// The node address whose lock this guard holds. The token
40    /// thus identifies *which* guard it tracks; `drop_requires`'s key
41    /// match prevents a guard's obligation from being used to drop a
42    /// different guard. The real lock-set ledger is `Guards::guards`;
43    /// this trait's discipline lifts the existing state-side discipline
44    /// onto the obligation token by carrying the locked address.
45    type Obligation = DropObligation<usize>;
46
47    open spec fn tracked_redeem_requires(self, s: Self::State) -> bool {
48        s.lock_held(self.inner.inner@.ptr.addr())
49    }
50
51    open spec fn tracked_redeem_ensures(
52        self,
53        s0: Self::State,
54        s1: Self::State,
55        obl: Self::Obligation,
56    ) -> bool {
57        &&& s1.guards == s0.guards.remove(self.inner.inner@.ptr.addr())
58        &&& obl.value() == self.inner.inner@.ptr.addr()
59    }
60
61    proof fn tracked_redeem(self, tracked s: &mut Self::State) -> (tracked obl: Self::Obligation) {
62        s.guards = s.guards.remove(self.inner.inner@.ptr.addr());
63        DropObligation::tracked_mint(self.inner.inner@.ptr.addr())
64    }
65
66    open spec fn drop_requires(self, s: Self::State, obl: Self::Obligation) -> bool {
67        &&& s.unlocked(self.inner.inner@.ptr.addr())
68        &&& obl.value() == self.inner.inner@.ptr.addr()
69    }
70
71    open spec fn drop_ensures(
72        self,
73        s0: Self::State,
74        s1: Self::State,
75        obl: Self::Obligation,
76    ) -> bool {
77        s1.guards == s0.guards.insert(self.inner.inner@.ptr.addr())
78    }
79}
80
81impl<C: PageTableConfig> PageTablePageMeta<C> {
82    pub open spec fn into_spec(self) -> StoredPageTablePageMeta {
83        StoredPageTablePageMeta {
84            nr_children: self.nr_children,
85            stray: self.stray,
86            level: self.level,
87            lock: self.lock,
88        }
89    }
90
91    #[verifier::when_used_as_spec(into_spec)]
92    pub fn into(self) -> (res: StoredPageTablePageMeta)
93        ensures
94            res == self.into_spec(),
95    {
96        StoredPageTablePageMeta {
97            nr_children: self.nr_children,
98            stray: self.stray,
99            level: self.level,
100            lock: self.lock,
101        }
102    }
103}
104
105impl StoredPageTablePageMeta {
106    pub open spec fn into_spec<C: PageTableConfig>(self) -> PageTablePageMeta<C> {
107        PageTablePageMeta::<C> {
108            nr_children: self.nr_children,
109            stray: self.stray,
110            level: self.level,
111            lock: self.lock,
112            _phantom: PhantomData,
113        }
114    }
115
116    #[verifier::when_used_as_spec(into_spec)]
117    pub fn into<C: PageTableConfig>(self) -> (res: PageTablePageMeta<C>)
118        ensures
119            res == self.into_spec::<C>(),
120    {
121        PageTablePageMeta::<C> {
122            nr_children: self.nr_children,
123            stray: self.stray,
124            level: self.level,
125            lock: self.lock,
126            _phantom: PhantomData,
127        }
128    }
129}
130
131pub uninterp spec fn drop_tree_spec<C: PageTableConfig>(
132    _page: Frame<PageTablePageMeta<C>>,
133) -> Frame<PageTablePageMeta<C>>;
134
135impl<C: PageTableConfig> Repr<MetaSlotStorage> for PageTablePageMeta<C> {
136    type ReprPerm = ();
137
138    open spec fn wf(r: MetaSlotStorage, perm: ()) -> bool {
139        matches!(r, MetaSlotStorage::PTNode(_))
140    }
141
142    open spec fn to_repr_spec(self, perm: ()) -> (MetaSlotStorage, ()) {
143        (MetaSlotStorage::PTNode(self.into_spec()), ())
144    }
145
146    #[verifier::external_body]
147    fn to_repr(self, Tracked(perm): Tracked<&mut ()>) -> MetaSlotStorage {
148        unimplemented!()
149    }
150
151    open spec fn from_repr_spec(r: MetaSlotStorage, perm: ()) -> Self {
152        match r {
153            MetaSlotStorage::PTNode(node) => node.into_spec::<C>(),
154            _ => arbitrary(),
155        }
156    }
157
158    #[verifier::external_body]
159    fn from_repr(r: MetaSlotStorage, Tracked(perm): Tracked<&()>) -> Self {
160        unimplemented!()
161    }
162
163    #[verifier::external_body]
164    fn from_borrowed<'a>(r: &'a MetaSlotStorage, Tracked(perm): Tracked<&'a ()>) -> &'a Self {
165        unimplemented!()
166    }
167
168    #[verifier::external_body]
169    fn from_borrowed_mut<'a>(
170        r: &'a mut MetaSlotStorage,
171        Tracked(perm): Tracked<&'a mut ()>,
172    ) -> &'a mut Self {
173        unimplemented!()
174    }
175
176    proof fn from_to_repr(self, perm: ()) {
177    }
178
179    proof fn to_from_repr(r: MetaSlotStorage, perm: ()) {
180        match r {
181            MetaSlotStorage::PTNode(node) => {},
182            _ => {
183                assert(false);
184            },
185        }
186    }
187
188    proof fn to_repr_wf(self, perm: ()) {
189    }
190}
191
192} // verus!
ostd/specs/mm/page_table/node/mod.rs

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