ostd/specs/mm/frame/linked_list/
linked_list_owners.rs

1use vstd::atomic::*;
2use vstd::prelude::*;
3use vstd::seq_lib::*;
4use vstd::simple_pptr::*;
5use vstd_extra::cast_ptr::Repr;
6use vstd_extra::ownership::*;
7
8use super::*;
9use crate::mm::frame::{AnyFrameMeta, CursorMut, Link, LinkedList, MetaSlot, UniqueFrameOwner};
10use crate::mm::Paddr;
11use crate::specs::arch::kspace::FRAME_METADATA_RANGE;
12use crate::specs::arch::mm::MAX_NR_PAGES;
13use crate::specs::mm::frame::mapping::META_SLOT_SIZE;
14
15verus! {
16
17pub ghost struct LinkModel {
18    pub paddr: Paddr,
19}
20
21impl Inv for LinkModel {
22    open spec fn inv(self) -> bool {
23        true
24    }
25}
26
27pub tracked struct LinkOwner {
28    pub paddr: Paddr,
29    pub in_list: u64,
30}
31
32impl Inv for LinkOwner {
33    open spec fn inv(self) -> bool {
34        true
35    }
36}
37
38impl View for LinkOwner {
39    type V = LinkModel;
40
41    open spec fn view(&self) -> Self::V {
42        LinkModel { paddr: self.paddr }
43    }
44}
45
46impl InvView for LinkOwner {
47    proof fn view_preserves_inv(self) {
48    }
49}
50
51// TODO: Technically M needs to be smaller than Link<M>, at minimum enough to fit the two pointers
52impl<M: AnyFrameMeta + Repr<MetaSlot>> OwnerOf for Link<M> {
53    type Owner = LinkOwner;
54
55    open spec fn wf(self, owner: Self::Owner) -> bool {
56        true
57        //        &&& owner.self_perm@.mem_contents().value() == self
58        //        &&& owner.next == self.next
59        //        &&& owner.prev == self.prev
60
61    }
62}
63
64impl<M: AnyFrameMeta + Repr<MetaSlot>> ModelOf for Link<M> {
65
66}
67
68pub ghost struct LinkedListModel {
69    pub list: Seq<LinkModel>,
70}
71
72impl LinkedListModel {
73    pub open spec fn front(self) -> Option<LinkModel> {
74        if self.list.len() > 0 {
75            Some(self.list[0])
76        } else {
77            None
78        }
79    }
80
81    pub open spec fn back(self) -> Option<LinkModel> {
82        if self.list.len() > 0 {
83            Some(self.list[self.list.len() - 1])
84        } else {
85            None
86        }
87    }
88}
89
90impl Inv for LinkedListModel {
91    open spec fn inv(self) -> bool {
92        true
93    }
94}
95
96#[rustc_has_incoherent_inherent_impls]
97pub tracked struct LinkedListOwner<M: AnyFrameMeta + Repr<MetaSlot>> {
98    pub list: Seq<LinkOwner>,
99    pub perms: Map<int, vstd_extra::cast_ptr::PointsTo<MetaSlot, Link<M>>>,
100    pub list_id: u64,
101}
102
103impl<M: AnyFrameMeta + Repr<MetaSlot>> Inv for LinkedListOwner<M> {
104    open spec fn inv(self) -> bool {
105        forall|i: int| 0 <= i < self.list.len() ==> self.inv_at(i)
106    }
107}
108
109impl<M: AnyFrameMeta + Repr<MetaSlot>> LinkedListOwner<M> {
110    pub open spec fn inv_at(self, i: int) -> bool {
111        &&& self.perms.contains_key(i)
112        &&& self.perms[i].addr() == self.list[i].paddr
113        &&& self.perms[i].points_to.addr() == self.list[i].paddr
114        &&& self.perms[i].wf()
115        &&& self.perms[i].addr() % META_SLOT_SIZE() == 0
116        &&& FRAME_METADATA_RANGE().start <= self.perms[i].addr() < FRAME_METADATA_RANGE().start
117            + MAX_NR_PAGES() * META_SLOT_SIZE()
118        &&& self.perms[i].is_init()
119        &&& self.perms[i].value().wf(self.list[i])
120        &&& i == 0 <==> self.perms[i].mem_contents().value().prev is None
121        &&& i == self.list.len() - 1 <==> self.perms[i].value().next is None
122        &&& 0 < i ==> self.perms[i].value().prev is Some && self.perms[i].value().prev.unwrap()
123            == self.perms[i - 1].pptr()
124        &&& i < self.list.len() - 1 ==> self.perms[i].value().next is Some
125            && self.perms[i].value().next.unwrap() == self.perms[i + 1].pptr()
126        &&& self.list[i].inv()
127        &&& self.list[i].in_list == self.list_id
128    }
129
130    pub open spec fn view_helper(owners: Seq<LinkOwner>) -> Seq<LinkModel>
131        decreases owners.len(),
132    {
133        if owners.len() == 0 {
134            Seq::<LinkModel>::empty()
135        } else {
136            seq![owners[0].view()].add(Self::view_helper(owners.remove(0)))
137        }
138    }
139
140    pub proof fn view_preserves_len(owners: Seq<LinkOwner>)
141        ensures
142            Self::view_helper(owners).len() == owners.len(),
143        decreases owners.len(),
144    {
145        if owners.len() == 0 {
146        } else {
147            Self::view_preserves_len(owners.remove(0))
148        }
149    }
150}
151
152impl<M: AnyFrameMeta + Repr<MetaSlot>> View for LinkedListOwner<M> {
153    type V = LinkedListModel;
154
155    open spec fn view(&self) -> Self::V {
156        LinkedListModel { list: Self::view_helper(self.list) }
157    }
158}
159
160impl<M: AnyFrameMeta + Repr<MetaSlot>> InvView for LinkedListOwner<M> {
161    proof fn view_preserves_inv(self) {
162    }
163}
164
165impl<M: AnyFrameMeta + Repr<MetaSlot>> LinkedListOwner<M> {
166    /*    pub open spec fn update_prev(links: Seq<LinkOwner<M>>, i: int, prev: Option<PPtr<Link<M>>>) -> Seq<LinkOwner<M>> {
167        let link = links[i];
168        let new_link = LinkOwner::<M> { prev: prev, ..link };
169        links.update(i, new_link)
170    }
171
172    pub open spec fn update_next(
173        links: Seq<LinkOwner<M>>,
174        i: int,
175        next: Option<PPtr<Link<M>>>,
176    ) -> Seq<LinkOwner<M>> {
177        let link = links[i];
178        let new_link = LinkOwner::<M> { next: next, ..link };
179        links.update(i, new_link)
180    }*/
181
182}
183
184impl<M: AnyFrameMeta + Repr<MetaSlot>> OwnerOf for LinkedList<M> {
185    type Owner = LinkedListOwner<M>;
186
187    open spec fn wf(self, owner: Self::Owner) -> bool {
188        &&& self.front is None <==> owner.list.len() == 0
189        &&& self.back is None <==> owner.list.len() == 0
190        &&& owner.list.len() > 0 ==> self.front is Some && self.front.unwrap().addr()
191            == owner.list[0].paddr && owner.perms[0].pptr() == self.front.unwrap()
192            && self.back is Some && self.back.unwrap().addr() == owner.list[owner.list.len()
193            - 1].paddr && owner.perms[owner.list.len() - 1].pptr() == self.back.unwrap()
194        &&& self.size == owner.list.len()
195        &&& self.list_id == owner.list_id
196    }
197}
198
199impl<M: AnyFrameMeta + Repr<MetaSlot>> ModelOf for LinkedList<M> {
200
201}
202
203#[rustc_has_incoherent_inherent_impls]
204pub ghost struct CursorModel {
205    pub ghost fore: Seq<LinkModel>,
206    pub ghost rear: Seq<LinkModel>,
207    pub ghost list_model: LinkedListModel,
208}
209
210impl Inv for CursorModel {
211    open spec fn inv(self) -> bool {
212        self.list_model.inv()
213    }
214}
215
216#[rustc_has_incoherent_inherent_impls]
217pub tracked struct CursorOwner<M: AnyFrameMeta + Repr<MetaSlot>> {
218    pub list_own: LinkedListOwner<M>,
219    pub list_perm: PointsTo<LinkedList<M>>,
220    pub index: int,
221}
222
223impl<M: AnyFrameMeta + Repr<MetaSlot>> Inv for CursorOwner<M> {
224    open spec fn inv(self) -> bool {
225        &&& 0 <= self.index <= self.length()
226        &&& self.list_own.inv()
227    }
228}
229
230impl<M: AnyFrameMeta + Repr<MetaSlot>> View for CursorOwner<M> {
231    type V = CursorModel;
232
233    open spec fn view(&self) -> Self::V {
234        let list = self.list_own.view();
235        CursorModel {
236            fore: list.list.take(self.index),
237            rear: list.list.skip(self.index),
238            list_model: list,
239        }
240    }
241}
242
243impl<M: AnyFrameMeta + Repr<MetaSlot>> InvView for CursorOwner<M> {
244    proof fn view_preserves_inv(self) {
245    }
246}
247
248impl<M: AnyFrameMeta + Repr<MetaSlot>> OwnerOf for CursorMut<M> {
249    type Owner = CursorOwner<M>;
250
251    open spec fn wf(self, owner: Self::Owner) -> bool {
252        &&& 0 <= owner.index < owner.length() ==> self.current.is_some()
253            && self.current.unwrap().addr() == owner.list_own.list[owner.index].paddr
254            && owner.list_own.perms[owner.index].pptr() == self.current.unwrap()
255        &&& owner.index == owner.list_own.list.len() ==> self.current.is_none()
256        &&& owner.list_perm.pptr() == self.list
257        &&& owner.list_perm.is_init()
258        &&& owner.list_perm.mem_contents().value().wf(owner.list_own)
259    }
260}
261
262impl<M: AnyFrameMeta + Repr<MetaSlot>> ModelOf for CursorMut<M> {
263
264}
265
266impl CursorModel {
267    pub open spec fn current(self) -> Option<LinkModel> {
268        if self.rear.len() > 0 {
269            Some(self.rear[0])
270        } else {
271            None
272        }
273    }
274}
275
276impl<M: AnyFrameMeta + Repr<MetaSlot>> CursorOwner<M> {
277    pub open spec fn length(self) -> int {
278        self.list_own.list.len() as int
279    }
280
281    pub open spec fn current(self) -> Option<LinkOwner> {
282        if 0 <= self.index < self.length() {
283            Some(self.list_own.list[self.index])
284        } else {
285            None
286        }
287    }
288
289    #[verifier::external_body]
290    pub fn list_insert(
291        Tracked(cursor): Tracked<&mut Self>,
292        Tracked(link): Tracked<&mut LinkOwner>,
293        Tracked(perm): Tracked<&vstd_extra::cast_ptr::PointsTo<MetaSlot, Link<M>>>,
294    )
295        ensures
296            cursor.list_own.list == old(cursor).list_own.list.insert(old(cursor).index, *old(link)),
297            cursor.list_own.list_id == old(cursor).list_own.list_id,
298            forall|idx: int| 0 <= idx < cursor.length() ==> cursor.list_own.perms.contains_key(idx),
299            forall|idx: int|
300                0 <= idx < cursor.index ==> cursor.list_own.perms[idx] == old(
301                    cursor,
302                ).list_own.perms[idx],
303            forall|idx: int|
304                old(cursor).index < idx <= old(cursor).length() ==> cursor.list_own.perms[idx]
305                    == old(cursor).list_own.perms[idx - 1],
306            cursor.list_own.perms[old(cursor).index] == perm,
307            cursor.index == old(cursor).index + 1,
308            cursor.list_perm == old(cursor).list_perm,
309            *link == *old(link),
310    {
311        unimplemented!()
312    }
313
314    pub open spec fn front_owner_spec(
315        list_own: LinkedListOwner<M>,
316        list_perm: PointsTo<LinkedList<M>>,
317    ) -> Self {
318        CursorOwner::<M> { list_own: list_own, list_perm: list_perm, index: 0 }
319    }
320
321    #[verifier::returns(proof)]
322    #[verifier::external_body]
323    pub proof fn front_owner(
324        list_own: LinkedListOwner<M>,
325        list_perm: PointsTo<LinkedList<M>>,
326    ) -> (res: Self)
327        ensures
328            res == Self::front_owner_spec(list_own, list_perm),
329    {
330        CursorOwner::<M> { list_own: list_own, list_perm: list_perm, index: 0 }
331    }
332
333    pub open spec fn back_owner_spec(
334        list_own: LinkedListOwner<M>,
335        list_perm: PointsTo<LinkedList<M>>,
336    ) -> Self {
337        CursorOwner::<M> {
338            list_own: list_own,
339            list_perm: list_perm,
340            index: if list_own.list.len() > 0 {
341                list_own.list.len() as int - 1
342            } else {
343                0
344            },
345        }
346    }
347
348    #[verifier::returns(proof)]
349    #[verifier::external_body]
350    pub proof fn back_owner(
351        list_own: LinkedListOwner<M>,
352        list_perm: PointsTo<LinkedList<M>>,
353    ) -> (res: Self)
354        ensures
355            res == Self::back_owner_spec(list_own, list_perm),
356    {
357        CursorOwner::<M> {
358            list_own: list_own,
359            list_perm: list_perm,
360            index: if list_own.list.len() > 0 {
361                list_own.list.len() as int - 1
362            } else {
363                0
364            },
365        }
366    }
367
368    pub open spec fn ghost_owner_spec(
369        list_own: LinkedListOwner<M>,
370        list_perm: PointsTo<LinkedList<M>>,
371    ) -> Self {
372        CursorOwner::<M> {
373            list_own: list_own,
374            list_perm: list_perm,
375            index: list_own.list.len() as int,
376        }
377    }
378
379    #[verifier::returns(proof)]
380    #[verifier::external_body]
381    pub proof fn ghost_owner(
382        list_own: LinkedListOwner<M>,
383        list_perm: PointsTo<LinkedList<M>>,
384    ) -> (res: Self)
385        ensures
386            res == Self::ghost_owner_spec(list_own, list_perm),
387    {
388        CursorOwner::<M> {
389            list_own: list_own,
390            list_perm: list_perm,
391            index: list_own.list.len() as int,
392        }
393    }
394}
395
396impl<M: AnyFrameMeta + Repr<MetaSlot>> UniqueFrameOwner<Link<M>> {
397    pub open spec fn frame_link_inv(&self) -> bool {
398        &&& self.meta_perm.value().prev is None
399        &&& self.meta_perm.value().next is None
400        &&& self.meta_own.paddr == self.meta_perm.addr()
401    }
402}
403
404} // verus!
ostd/specs/mm/frame/linked_list/linked_list_owners.rs

ostd/specs/mm/frame/linked_list/
linked_list_owners.rs
