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::*;
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
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    pub open spec fn move_prev_spec(self) -> Self {
39        if self.list_model.list.len() > 0 {
40            if self.fore.len() > 0 {
41                let cur = self.fore[self.fore.len() - 1];
42                Self {
43                    fore: self.fore.remove(self.fore.len() - 1),
44                    rear: self.rear.insert(0, cur),
45                    list_model: self.list_model,
46                }
47            } else {
48                Self {
49                    fore: self.rear,
50                    rear: Seq::<LinkModel>::empty(),
51                    list_model: self.list_model,
52                }
53            }
54        } else {
55            self
56        }
57    }
58
59    pub open spec fn remove(self) -> Self {
60        let rear = self.rear.remove(0);
61
62        Self {
63            fore: self.fore,
64            rear: rear,
65            list_model: LinkedListModel { list: self.fore.add(rear) },
66        }
67    }
68
69    pub open spec fn insert(self, link: LinkModel) -> Self {
70        let fore = self.fore.insert(self.fore.len() as int, link);
71
72        Self {
73            fore: fore,
74            rear: self.rear,
75            list_model: LinkedListModel { list: fore.add(self.rear) },
76        }
77    }
78}
79
80impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> CursorOwner<M> {
81    pub open spec fn remove_owner_spec(self, post: Self) -> bool
82        recommends
83            self.index < self.length(),
84    {
85        &&& post.list_own.list == self.list_own.list.remove(self.index)
86        &&& post.index == self.index
87    }
88
89    pub proof fn remove_owner_spec_implies_model_spec(self, post: Self)
90        requires
91            self.remove_owner_spec(post),
92            0 <= self.index < self.length(),
93        ensures
94            post@ == self@.remove(),
95    {
96        let idx = self.index;
97        let s = self.list_own.list;
98        let ps = post.list_own.list;
99
100        LinkedListOwner::<M>::view_preserves_len(s);
101        LinkedListOwner::<M>::view_preserves_len(ps);
102
103        let vh_s = LinkedListOwner::<M>::view_helper(s);
104        let vh_ps = LinkedListOwner::<M>::view_helper(ps);
105
106        assert(post@.fore =~= self@.fore) by {
107            assert forall |j: int| 0 <= j < vh_ps.take(idx).len() implies
108                vh_ps.take(idx)[j] == vh_s.take(idx)[j]
109            by {
110                LinkedListOwner::<M>::view_helper_index(ps, j);
111                LinkedListOwner::<M>::view_helper_index(s, j);
112            };
113        };
114
115        assert(post@.rear =~= self@.remove().rear) by {
116            assert forall |j: int| 0 <= j < vh_ps.skip(idx).len() implies
117                #[trigger] vh_ps.skip(idx)[j] == vh_s.skip(idx).remove(0)[j]
118            by {
119                LinkedListOwner::<M>::view_helper_index(ps, idx + j);
120                LinkedListOwner::<M>::view_helper_index(s, idx + j + 1);
121            };
122        };
123
124        assert forall |j: int| 0 <= j < vh_ps.len() implies
125            #[trigger] vh_ps[j] == vh_s.take(idx).add(vh_s.skip(idx).remove(0))[j]
126        by {
127            LinkedListOwner::<M>::view_helper_index(ps, j);
128            if j < idx {
129                LinkedListOwner::<M>::view_helper_index(s, j);
130            } else {
131                LinkedListOwner::<M>::view_helper_index(s, j + 1);
132            }
133        };
134        assert(vh_ps =~= vh_s.take(idx).add(vh_s.skip(idx).remove(0)));
135        assert(post@.list_model == self@.remove().list_model);
136    }
137
138    pub open spec fn insert_owner_spec(self, link: LinkOwner, post: Self) -> bool
139        recommends
140            self.index < self.length(),
141    {
142        &&& post.list_own.list == self.list_own.list.insert(self.index, link)
143        &&& post.list_own.list_id == self.list_own.list_id
144        &&& post.index == self.index + 1
145    }
146
147    pub proof fn insert_owner_spec_implies_model_spec(self, link: LinkOwner, post: Self)
148        requires
149            self.insert_owner_spec(link, post),
150            0 <= self.index <= self.length(),
151        ensures
152            post@ == self@.insert(link@),
153    {
154        let idx = self.index;
155        let s = self.list_own.list;
156        let ps = post.list_own.list;
157
158        LinkedListOwner::<M>::view_preserves_len(s);
159        LinkedListOwner::<M>::view_preserves_len(ps);
160        LinkedListOwner::<M>::view_helper_insert(s, idx, link);
161
162        let vh_s = LinkedListOwner::<M>::view_helper(s);
163        let vh_ps = LinkedListOwner::<M>::view_helper(ps);
164
165        assert(post@.fore =~= self@.insert(link@).fore) by {
166            assert forall |j: int| 0 <= j < vh_ps.take(idx + 1).len() implies
167                vh_ps.take(idx + 1)[j] == vh_s.take(idx).insert(idx as int, link@)[j]
168            by {
169                LinkedListOwner::<M>::view_helper_index(ps, j);
170                if j < idx {
171                    LinkedListOwner::<M>::view_helper_index(s, j);
172                }
173            };
174        };
175
176        assert(post@.rear =~= self@.insert(link@).rear) by {
177            assert forall |j: int| 0 <= j < vh_ps.skip(idx + 1).len() implies
178                vh_ps.skip(idx + 1)[j] == vh_s.skip(idx)[j]
179            by {
180                LinkedListOwner::<M>::view_helper_index(ps, idx + 1 + j);
181                LinkedListOwner::<M>::view_helper_index(s, idx + j);
182            };
183        };
184
185        let new_fore = vh_s.take(idx).insert(idx as int, link@);
186        assert forall |j: int| 0 <= j < vh_ps.len() implies
187            #[trigger] vh_ps[j] == new_fore.add(vh_s.skip(idx))[j]
188        by {
189            LinkedListOwner::<M>::view_helper_index(ps, j);
190            if j < idx {
191                LinkedListOwner::<M>::view_helper_index(s, j);
192            } else if j > idx {
193                LinkedListOwner::<M>::view_helper_index(s, j - 1);
194            }
195        };
196        assert(vh_ps =~= new_fore.add(vh_s.skip(idx)));
197        assert(post@.list_model == self@.insert(link@).list_model);
198    }
199
200    pub open spec fn move_next_owner_spec(self) -> Self {
201        if self.length() == 0 {
202            self
203        } else if self.index == self.length() {
204            Self { list_own: self.list_own, index: 0 }
205        } else if self.index == self.length() - 1 {
206            Self { list_own: self.list_own, index: self.index + 1 }
207        } else {
208            Self { list_own: self.list_own, index: self.index + 1 }
209        }
210    }
211
212    pub open spec fn move_prev_owner_spec(self) -> Self {
213        if self.length() == 0 {
214            self
215        } else if self.index == self.length() {
216            Self { list_own: self.list_own, index: self.index - 1 }
217        } else if self.index == 0 {
218            Self { list_own: self.list_own, index: self.length() }
219        } else {
220            Self { list_own: self.list_own, index: self.index - 1 }
221        }
222    }
223}
224
225} // verus!
ostd/specs/mm/frame/linked_list/linked_list_specs.rs

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