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

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

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