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

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

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