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

1use vstd::prelude::*;
2
3use vstd_extra::cast_ptr::*;
4use vstd_extra::ownership::*;
5use vstd_extra::prelude::*;
6
7use super::linked_list_owners::{CursorModel, CursorOwner, LinkModel, LinkOwner, LinkedListModel};
8use crate::mm::frame::linked_list::Link;
9use crate::mm::frame::*;
10use crate::mm::{Paddr, PagingLevel, Vaddr};
11use crate::specs::arch::mm::{MAX_NR_PAGES, MAX_PADDR, PAGE_SIZE};
12
13verus! {
14
15impl CursorModel {
16    #[rustc_allow_incoherent_impl]
17    pub open spec fn move_next_spec(self) -> Self {
18        if self.list_model.list.len() > 0 {
19            if self.rear.len() > 0 {
20                let cur = self.rear[0];
21                Self {
22                    fore: self.fore.insert(self.fore.len() as int, cur),
23                    rear: self.rear.remove(0),
24                    list_model: self.list_model,
25                }
26            } else {
27                Self {
28                    fore: Seq::<LinkModel>::empty(),
29                    rear: self.fore,
30                    list_model: self.list_model,
31                }
32            }
33        } else {
34            self
35        }
36    }
37
38    #[rustc_allow_incoherent_impl]
39    pub open spec fn move_prev_spec(self) -> Self {
40        if self.list_model.list.len() > 0 {
41            if self.fore.len() > 0 {
42                let cur = self.fore[self.fore.len() - 1];
43                Self {
44                    fore: self.fore.remove(self.fore.len() - 1),
45                    rear: self.rear.insert(0, cur),
46                    list_model: self.list_model,
47                }
48            } else {
49                Self {
50                    fore: self.rear,
51                    rear: Seq::<LinkModel>::empty(),
52                    list_model: self.list_model,
53                }
54            }
55        } else {
56            self
57        }
58    }
59
60    #[rustc_allow_incoherent_impl]
61    pub open spec fn remove(self) -> Self {
62        let rear = self.rear.remove(0);
63
64        Self {
65            fore: self.fore,
66            rear: rear,
67            list_model: LinkedListModel { list: self.fore.add(rear) },
68        }
69    }
70
71    #[rustc_allow_incoherent_impl]
72    pub open spec fn insert(self, link: LinkModel) -> Self {
73        let fore = self.fore.insert(self.fore.len() - 1, link);
74
75        Self {
76            fore: fore,
77            rear: self.rear,
78            list_model: LinkedListModel { list: fore.add(self.rear) },
79        }
80    }
81}
82
83impl<M: AnyFrameMeta + Repr<MetaSlot>> CursorOwner<M> {
84    #[rustc_allow_incoherent_impl]
85    pub open spec fn remove_owner_spec(self, post: Self) -> bool
86        recommends
87            self.index < self.length(),
88    {
89        &&& post.list_own.list == self.list_own.list.remove(self.index)
90        &&& post.index == self.index
91    }
92
93    #[rustc_allow_incoherent_impl]
94    pub proof fn remove_owner_spec_implies_model_spec(self, post: Self)
95        requires
96            self.remove_owner_spec(post),
97        ensures
98            post@ == self@.remove(),
99    {
100        admit()
101    }
102
103    #[rustc_allow_incoherent_impl]
104    pub open spec fn insert_owner_spec(self, link: LinkOwner, post: Self) -> bool
105        recommends
106            self.index < self.length(),
107    {
108        &&& post.list_own.list == self.list_own.list.insert(self.index, link)
109        &&& post.list_own.list_id == self.list_own.list_id
110        &&& post.index == self.index + 1
111    }
112
113    #[rustc_allow_incoherent_impl]
114    pub proof fn insert_owner_spec_implies_model_spec(self, link: LinkOwner, post: Self)
115        requires
116            self.insert_owner_spec(link, post),
117        ensures
118            post@ == self@.insert(link@),
119    {
120        admit()
121    }
122
123    #[rustc_allow_incoherent_impl]
124    pub open spec fn move_next_owner_spec(self) -> Self {
125        if self.length() == 0 {
126            self
127        } else if self.index == self.length() {
128            Self { list_own: self.list_own, list_perm: self.list_perm, index: 0 }
129        } else if self.index == self.length() - 1 {
130            Self { list_own: self.list_own, list_perm: self.list_perm, index: self.index + 1 }
131        } else {
132            Self { list_own: self.list_own, list_perm: self.list_perm, index: self.index + 1 }
133        }
134    }
135
136    #[rustc_allow_incoherent_impl]
137    pub open spec fn move_prev_owner_spec(self) -> Self {
138        if self.length() == 0 {
139            self
140        } else if self.index == self.length() {
141            Self { list_own: self.list_own, list_perm: self.list_perm, index: self.index - 1 }
142        } else if self.index == 0 {
143            Self { list_own: self.list_own, list_perm: self.list_perm, index: self.length() }
144        } else {
145            Self { list_own: self.list_own, list_perm: self.list_perm, index: self.index - 1 }
146        }
147    }
148}
149
150} // verus!
ostd/specs/mm/frame/linked_list/linked_list_specs.rs

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