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        &&& post.list_own.list == self.list_own.list.remove(self.index)
80        &&& post.index == self.index
81    }
82
83    pub proof fn remove_owner_spec_implies_model_spec(self, post: Self)
84        requires
85            self.remove_owner_spec(post),
86            0 <= self.index < self.length(),
87        ensures
88            post@ == self@.remove(),
89    {
90        let idx = self.index;
91        let s = self.list_own.list;
92        let ps = post.list_own.list;
93
94        LinkedListOwner::<M>::view_preserves_len(s);
95        LinkedListOwner::<M>::view_preserves_len(ps);
96
97        let vh_s = LinkedListOwner::<M>::view_helper(s);
98        let vh_ps = LinkedListOwner::<M>::view_helper(ps);
99
100        assert(post@.fore == self@.fore) by {
101            assert forall|j: int| 0 <= j < vh_ps.take(idx).len() implies vh_ps.take(idx)[j]
102                == vh_s.take(idx)[j] by {
103                LinkedListOwner::<M>::view_helper_index(ps, j);
104                LinkedListOwner::<M>::view_helper_index(s, j);
105            };
106        };
107
108        assert(post@.rear == self@.remove().rear) by {
109            assert forall|j: int| 0 <= j < vh_ps.skip(idx).len() implies #[trigger] vh_ps.skip(
110                idx,
111            )[j] == vh_s.skip(idx).remove(0)[j] by {
112                LinkedListOwner::<M>::view_helper_index(ps, idx + j);
113                LinkedListOwner::<M>::view_helper_index(s, idx + j + 1);
114            };
115        };
116
117        assert forall|j: int| 0 <= j < vh_ps.len() implies #[trigger] vh_ps[j] == vh_s.take(
118            idx,
119        ).add(vh_s.skip(idx).remove(0))[j] by {
120            LinkedListOwner::<M>::view_helper_index(ps, j);
121            if j < idx {
122                LinkedListOwner::<M>::view_helper_index(s, j);
123            } else {
124                LinkedListOwner::<M>::view_helper_index(s, j + 1);
125            }
126        };
127        assert(vh_ps == vh_s.take(idx).add(vh_s.skip(idx).remove(0)));
128        assert(post@.list_model == self@.remove().list_model);
129    }
130
131    pub open spec fn insert_owner_spec(self, link: LinkOwner, post: Self) -> bool {
132        // The list model (`view_helper`) depends only on the element sequence,
133        // not on `list_id`, so this carries no `list_id` clause — letting it
134        // hold even when the insert mints a fresh id for a previously-empty list.
135        &&& post.list_own.list == self.list_own.list.insert(self.index, link)
136        &&& post.index == self.index + 1
137    }
138
139    pub proof fn insert_owner_spec_implies_model_spec(self, link: LinkOwner, post: Self)
140        requires
141            self.insert_owner_spec(link, post),
142            0 <= self.index <= self.length(),
143        ensures
144            post@ == self@.insert(link@),
145    {
146        let idx = self.index;
147        let s = self.list_own.list;
148        let ps = post.list_own.list;
149
150        LinkedListOwner::<M>::view_preserves_len(s);
151        LinkedListOwner::<M>::view_preserves_len(ps);
152        LinkedListOwner::<M>::view_helper_insert(s, idx, link);
153
154        let vh_s = LinkedListOwner::<M>::view_helper(s);
155        let vh_ps = LinkedListOwner::<M>::view_helper(ps);
156
157        assert(post@.fore == self@.insert(link@).fore) by {
158            assert forall|j: int| 0 <= j < vh_ps.take(idx + 1).len() implies vh_ps.take(idx + 1)[j]
159                == vh_s.take(idx).insert(idx as int, link@)[j] by {
160                LinkedListOwner::<M>::view_helper_index(ps, j);
161                if j < idx {
162                    LinkedListOwner::<M>::view_helper_index(s, j);
163                }
164            };
165        };
166
167        assert(post@.rear == self@.insert(link@).rear) by {
168            assert forall|j: int| 0 <= j < vh_ps.skip(idx + 1).len() implies vh_ps.skip(idx + 1)[j]
169                == vh_s.skip(idx)[j] by {
170                LinkedListOwner::<M>::view_helper_index(ps, idx + 1 + j);
171                LinkedListOwner::<M>::view_helper_index(s, idx + j);
172            };
173        };
174
175        let new_fore = vh_s.take(idx).insert(idx as int, link@);
176        assert forall|j: int| 0 <= j < vh_ps.len() implies #[trigger] vh_ps[j] == new_fore.add(
177            vh_s.skip(idx),
178        )[j] 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                LinkedListOwner::<M>::view_helper_index(s, j - 1);
184            }
185        };
186        assert(vh_ps == new_fore.add(vh_s.skip(idx)));
187        assert(post@.list_model == self@.insert(link@).list_model);
188    }
189
190    pub open spec fn move_next_owner_spec(self) -> Self {
191        if self.length() == 0 {
192            self
193        } else if self.index == self.length() {
194            Self { list_own: self.list_own, index: 0 }
195        } else if self.index == self.length() - 1 {
196            Self { list_own: self.list_own, index: self.index + 1 }
197        } else {
198            Self { list_own: self.list_own, index: self.index + 1 }
199        }
200    }
201
202    pub open spec fn move_prev_owner_spec(self) -> Self {
203        if self.length() == 0 {
204            self
205        } else if self.index == self.length() {
206            Self { list_own: self.list_own, index: self.index - 1 }
207        } else if self.index == 0 {
208            Self { list_own: self.list_own, index: self.length() }
209        } else {
210            Self { list_own: self.list_own, index: self.index - 1 }
211        }
212    }
213}
214
215} // verus!
ostd/specs/mm/frame/linked_list/linked_list_specs.rs

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