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

1use vstd::prelude::*;
2use vstd_extra::{cast_ptr::*, ownership::*, prelude::*};
3
4use crate::mm::{
5    Paddr, PagingLevel, Vaddr,
6    frame::{linked_list::Link, *},
7};
8
9use super::linked_list_owners::*;
10
11verus! {
12
13impl CursorModel {
14    pub open spec fn move_next_spec(self) -> Self {
15        if self.list_model.list.len() > 0 {
16            if self.rear.len() > 0 {
17                let cur = self.rear[0];
18                Self {
19                    fore: self.fore.insert(self.fore.len() as int, cur),
20                    rear: self.rear.remove(0),
21                    list_model: self.list_model,
22                }
23            } else {
24                Self {
25                    fore: Seq::<LinkModel>::empty(),
26                    rear: self.fore,
27                    list_model: self.list_model,
28                }
29            }
30        } else {
31            self
32        }
33    }
34
35    pub open spec fn move_prev_spec(self) -> Self {
36        if self.list_model.list.len() > 0 {
37            if self.fore.len() > 0 {
38                let cur = self.fore[self.fore.len() - 1];
39                Self {
40                    fore: self.fore.remove(self.fore.len() - 1),
41                    rear: self.rear.insert(0, cur),
42                    list_model: self.list_model,
43                }
44            } else {
45                Self {
46                    fore: self.rear,
47                    rear: Seq::<LinkModel>::empty(),
48                    list_model: self.list_model,
49                }
50            }
51        } else {
52            self
53        }
54    }
55
56    pub open spec fn remove(self) -> Self {
57        let rear = self.rear.remove(0);
58
59        Self {
60            fore: self.fore,
61            rear: rear,
62            list_model: LinkedListModel { list: self.fore.add(rear) },
63        }
64    }
65
66    pub open spec fn insert(self, link: LinkModel) -> Self {
67        let fore = self.fore.insert(self.fore.len() as int, link);
68
69        Self {
70            fore: fore,
71            rear: self.rear,
72            list_model: LinkedListModel { list: fore.add(self.rear) },
73        }
74    }
75}
76
77impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> CursorOwner<M> {
78    pub open spec fn remove_owner_spec(self, post: Self) -> bool
79        recommends
80            self.index < self.length(),
81    {
82        &&& post.list_own.list == self.list_own.list.remove(self.index)
83        &&& post.index == self.index
84    }
85
86    pub proof fn remove_owner_spec_implies_model_spec(self, post: Self)
87        requires
88            self.remove_owner_spec(post),
89            0 <= self.index < self.length(),
90        ensures
91            post@ == self@.remove(),
92    {
93        let idx = self.index;
94        let s = self.list_own.list;
95        let ps = post.list_own.list;
96
97        LinkedListOwner::<M>::view_preserves_len(s);
98        LinkedListOwner::<M>::view_preserves_len(ps);
99
100        let vh_s = LinkedListOwner::<M>::view_helper(s);
101        let vh_ps = LinkedListOwner::<M>::view_helper(ps);
102
103        assert(post@.fore == self@.fore) by {
104            assert forall|j: int| 0 <= j < vh_ps.take(idx).len() implies vh_ps.take(idx)[j]
105                == vh_s.take(idx)[j] by {
106                LinkedListOwner::<M>::view_helper_index(ps, j);
107                LinkedListOwner::<M>::view_helper_index(s, j);
108            };
109        };
110
111        assert(post@.rear == self@.remove().rear) by {
112            assert forall|j: int| 0 <= j < vh_ps.skip(idx).len() implies #[trigger] vh_ps.skip(
113                idx,
114            )[j] == vh_s.skip(idx).remove(0)[j] by {
115                LinkedListOwner::<M>::view_helper_index(ps, idx + j);
116                LinkedListOwner::<M>::view_helper_index(s, idx + j + 1);
117            };
118        };
119
120        assert forall|j: int| 0 <= j < vh_ps.len() implies #[trigger] vh_ps[j] == vh_s.take(
121            idx,
122        ).add(vh_s.skip(idx).remove(0))[j] by {
123            LinkedListOwner::<M>::view_helper_index(ps, j);
124            if j < idx {
125                LinkedListOwner::<M>::view_helper_index(s, j);
126            } else {
127                LinkedListOwner::<M>::view_helper_index(s, j + 1);
128            }
129        };
130        assert(vh_ps == vh_s.take(idx).add(vh_s.skip(idx).remove(0)));
131        assert(post@.list_model == self@.remove().list_model);
132    }
133
134    pub open spec fn insert_owner_spec(self, link: LinkOwner, post: Self) -> bool
135        recommends
136            self.index < self.length(),
137    {
138        // The list model (`view_helper`) depends only on the element sequence,
139        // not on `list_id`, so this carries no `list_id` clause — letting it
140        // hold even when the insert mints a fresh id for a previously-empty list.
141        &&& post.list_own.list == self.list_own.list.insert(self.index, link)
142        &&& post.index == self.index + 1
143    }
144
145    pub proof fn insert_owner_spec_implies_model_spec(self, link: LinkOwner, post: Self)
146        requires
147            self.insert_owner_spec(link, post),
148            0 <= self.index <= self.length(),
149        ensures
150            post@ == self@.insert(link@),
151    {
152        let idx = self.index;
153        let s = self.list_own.list;
154        let ps = post.list_own.list;
155
156        LinkedListOwner::<M>::view_preserves_len(s);
157        LinkedListOwner::<M>::view_preserves_len(ps);
158        LinkedListOwner::<M>::view_helper_insert(s, idx, link);
159
160        let vh_s = LinkedListOwner::<M>::view_helper(s);
161        let vh_ps = LinkedListOwner::<M>::view_helper(ps);
162
163        assert(post@.fore == self@.insert(link@).fore) by {
164            assert forall|j: int| 0 <= j < vh_ps.take(idx + 1).len() implies vh_ps.take(idx + 1)[j]
165                == vh_s.take(idx).insert(idx as int, link@)[j] by {
166                LinkedListOwner::<M>::view_helper_index(ps, j);
167                if j < idx {
168                    LinkedListOwner::<M>::view_helper_index(s, j);
169                }
170            };
171        };
172
173        assert(post@.rear == self@.insert(link@).rear) by {
174            assert forall|j: int| 0 <= j < vh_ps.skip(idx + 1).len() implies vh_ps.skip(idx + 1)[j]
175                == vh_s.skip(idx)[j] by {
176                LinkedListOwner::<M>::view_helper_index(ps, idx + 1 + j);
177                LinkedListOwner::<M>::view_helper_index(s, idx + j);
178            };
179        };
180
181        let new_fore = vh_s.take(idx).insert(idx as int, link@);
182        assert forall|j: int| 0 <= j < vh_ps.len() implies #[trigger] vh_ps[j] == new_fore.add(
183            vh_s.skip(idx),
184        )[j] by {
185            LinkedListOwner::<M>::view_helper_index(ps, j);
186            if j < idx {
187                LinkedListOwner::<M>::view_helper_index(s, j);
188            } else if j > idx {
189                LinkedListOwner::<M>::view_helper_index(s, j - 1);
190            }
191        };
192        assert(vh_ps == new_fore.add(vh_s.skip(idx)));
193        assert(post@.list_model == self@.insert(link@).list_model);
194    }
195
196    pub open spec fn move_next_owner_spec(self) -> Self {
197        if self.length() == 0 {
198            self
199        } else if self.index == self.length() {
200            Self { list_own: self.list_own, index: 0 }
201        } else if self.index == self.length() - 1 {
202            Self { list_own: self.list_own, index: self.index + 1 }
203        } else {
204            Self { list_own: self.list_own, index: self.index + 1 }
205        }
206    }
207
208    pub open spec fn move_prev_owner_spec(self) -> Self {
209        if self.length() == 0 {
210            self
211        } else if self.index == self.length() {
212            Self { list_own: self.list_own, index: self.index - 1 }
213        } else if self.index == 0 {
214            Self { list_own: self.list_own, index: self.length() }
215        } else {
216            Self { list_own: self.list_own, index: self.index - 1 }
217        }
218    }
219}
220
221} // verus!
ostd/specs/mm/frame/linked_list/linked_list_specs.rs

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