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

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