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; // == s.remove(idx)
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        // fore: vh_ps.take(idx) =~= vh_s.take(idx)
107        assert(post@.fore =~= self@.fore) by {
108            assert forall |j: int| 0 <= j < vh_ps.take(idx).len() implies
109                vh_ps.take(idx)[j] == vh_s.take(idx)[j]
110            by {
111                LinkedListOwner::<M>::view_helper_index(ps, j);
112                LinkedListOwner::<M>::view_helper_index(s, j);
113            };
114        };
115
116        // rear: vh_ps.skip(idx) =~= vh_s.skip(idx).remove(0)
117        assert(post@.rear =~= self@.remove().rear) by {
118            assert forall |j: int| 0 <= j < vh_ps.skip(idx).len() implies
119                #[trigger] vh_ps.skip(idx)[j] == vh_s.skip(idx).remove(0)[j]
120            by {
121                LinkedListOwner::<M>::view_helper_index(ps, idx + j);
122                LinkedListOwner::<M>::view_helper_index(s, idx + j + 1);
123            };
124        };
125
126        // list_model: vh_ps =~= vh_s.take(idx).add(vh_s.skip(idx).remove(0))
127        assert(post@.list_model == self@.remove().list_model) by {
128            assert(vh_ps =~= vh_s.take(idx).add(vh_s.skip(idx).remove(0))) by {
129                assert forall |j: int| 0 <= j < vh_ps.len() implies
130                    #[trigger] vh_ps[j] == vh_s.take(idx).add(vh_s.skip(idx).remove(0))[j]
131                by {
132                    LinkedListOwner::<M>::view_helper_index(ps, j);
133                    if j < idx {
134                        LinkedListOwner::<M>::view_helper_index(s, j);
135                    } else {
136                        LinkedListOwner::<M>::view_helper_index(s, j + 1);
137                    }
138                };
139            };
140        };
141    }
142
143    pub open spec fn insert_owner_spec(self, link: LinkOwner, post: Self) -> bool
144        recommends
145            self.index < self.length(),
146    {
147        &&& post.list_own.list == self.list_own.list.insert(self.index, link)
148        &&& post.list_own.list_id == self.list_own.list_id
149        &&& post.index == self.index + 1
150    }
151
152    pub proof fn insert_owner_spec_implies_model_spec(self, link: LinkOwner, post: Self)
153        requires
154            self.insert_owner_spec(link, post),
155            0 <= self.index <= self.length(),
156        ensures
157            post@ == self@.insert(link@),
158    {
159        let idx = self.index;
160        let s = self.list_own.list;
161        let ps = post.list_own.list; // == s.insert(idx, link)
162
163        LinkedListOwner::<M>::view_preserves_len(s);
164        LinkedListOwner::<M>::view_preserves_len(ps);
165        LinkedListOwner::<M>::view_helper_insert(s, idx, link);
166
167        let vh_s = LinkedListOwner::<M>::view_helper(s);
168        let vh_ps = LinkedListOwner::<M>::view_helper(ps);
169
170        // From view_helper_insert: vh_ps =~= vh_s.insert(idx, link@)
171
172        // fore: vh_ps.take(idx + 1) =~= vh_s.take(idx).insert(idx, link@) = vh_s.take(idx).push(link@)
173        assert(post@.fore =~= self@.insert(link@).fore) by {
174            // post@.fore = vh_ps.take(idx + 1)
175            // self@.insert(link@).fore = vh_s.take(idx).insert(idx as int, link@)
176            assert forall |j: int| 0 <= j < vh_ps.take(idx + 1).len() implies
177                vh_ps.take(idx + 1)[j] == vh_s.take(idx).insert(idx as int, link@)[j]
178            by {
179                LinkedListOwner::<M>::view_helper_index(ps, j);
180                if j < idx {
181                    LinkedListOwner::<M>::view_helper_index(s, j);
182                } else if j == idx {
183                    // ps[idx] == link, and vh_s.take(idx).insert(idx, link@)[idx] == link@
184                } else {
185                    // j > idx is impossible since j < idx + 1 means j <= idx
186                }
187            };
188        };
189
190        // rear: vh_ps.skip(idx + 1) =~= vh_s.skip(idx)
191        assert(post@.rear =~= self@.insert(link@).rear) by {
192            // post@.rear = vh_ps.skip(idx + 1)
193            // self@.insert(link@).rear = self@.rear = vh_s.skip(idx)
194            assert forall |j: int| 0 <= j < vh_ps.skip(idx + 1).len() implies
195                vh_ps.skip(idx + 1)[j] == vh_s.skip(idx)[j]
196            by {
197                LinkedListOwner::<M>::view_helper_index(ps, idx + 1 + j);
198                LinkedListOwner::<M>::view_helper_index(s, idx + j);
199            };
200        };
201
202        // list_model: vh_ps =~= vh_s.take(idx).insert(idx, link@).add(vh_s.skip(idx))
203        assert(post@.list_model == self@.insert(link@).list_model) by {
204            let new_fore = vh_s.take(idx).insert(idx as int, link@);
205            assert(vh_ps =~= new_fore.add(vh_s.skip(idx))) by {
206                assert forall |j: int| 0 <= j < vh_ps.len() implies
207                    #[trigger] vh_ps[j] == new_fore.add(vh_s.skip(idx))[j]
208                by {
209                    LinkedListOwner::<M>::view_helper_index(ps, j);
210                    if j < idx {
211                        LinkedListOwner::<M>::view_helper_index(s, j);
212                    } else if j == idx {
213                        // ps[idx] == link, new_fore[idx] == link@
214                    } else {
215                        LinkedListOwner::<M>::view_helper_index(s, j - 1);
216                    }
217                };
218            };
219        };
220    }
221
222    pub open spec fn move_next_owner_spec(self) -> Self {
223        if self.length() == 0 {
224            self
225        } else if self.index == self.length() {
226            Self { list_own: self.list_own, list_perm: self.list_perm, index: 0 }
227        } else if self.index == self.length() - 1 {
228            Self { list_own: self.list_own, list_perm: self.list_perm, index: self.index + 1 }
229        } else {
230            Self { list_own: self.list_own, list_perm: self.list_perm, index: self.index + 1 }
231        }
232    }
233
234    pub open spec fn move_prev_owner_spec(self) -> Self {
235        if self.length() == 0 {
236            self
237        } else if self.index == self.length() {
238            Self { list_own: self.list_own, list_perm: self.list_perm, index: self.index - 1 }
239        } else if self.index == 0 {
240            Self { list_own: self.list_own, list_perm: self.list_perm, index: self.length() }
241        } else {
242            Self { list_own: self.list_own, list_perm: self.list_perm, index: self.index - 1 }
243        }
244    }
245}
246
247} // verus!
ostd/specs/mm/frame/linked_list/linked_list_specs.rs

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