ostd/specs/mm/page_table/cursor/
split_while_huge_lemmas.rs

1use vstd::{prelude::*, set_lib::*};
2use vstd_extra::{arithmetic::*, ghost_tree::*, ownership::*};
3
4use crate::specs::{
5    arch::*,
6    mm::page_table::{cursor::owners::*, owners::PageTableOwner, *},
7};
8
9use crate::arch::mm::PagingConsts;
10use crate::mm::{
11    Paddr, PagingConstsTrait, PagingLevel, Vaddr, page_prop::PageProperty, page_size, page_table::*,
12};
13
14verus! {
15
16broadcast use group_ghost_tree_lemmas;
17
18impl<C: PageTableConfig> CursorView<C> {
19    proof fn lemma_split_index_inv(m: Mapping, new_size: usize, k: int)
20        requires
21            m.inv(),
22            new_size > 0,
23            m.page_size % new_size == 0,
24            set![4096usize, 2097152, 1073741824].contains(new_size),
25            m.va_range.start % new_size as int == 0,
26            0 <= k < m.page_size as int / new_size as int,
27        ensures
28            Self::split_index(m, new_size, k as usize).inv(),
29            m.va_range.start <= Self::split_index(m, new_size, k as usize).va_range.start,
30            Self::split_index(m, new_size, k as usize).va_range.end <= m.va_range.end,
31    {
32        let ps = m.page_size as int;
33        let ns = new_size as int;
34        let count = ps / ns;
35        let sub = Self::split_index(m, new_size, k as usize);
36
37        vstd::arithmetic::div_mod::lemma_fundamental_div_mod(ps, ns);
38        assert(ps == count * ns) by {
39            vstd::arithmetic::mul::lemma_mul_is_commutative(ns, count);
40        };
41        vstd::arithmetic::mul::lemma_mul_inequality(k + 1, count, ns);
42        vstd::arithmetic::mul::lemma_mul_is_distributive_add_other_way(ns, k, 1);
43
44        vstd::arithmetic::div_mod::lemma_mod_mod(m.pa_range.start as int, ns, count);
45        assert((m.pa_range.start as int) % ns == 0);
46        vstd::arithmetic::div_mod::lemma_mod_multiples_basic(k, ns);
47        vstd::arithmetic::div_mod::lemma_mod_multiples_basic(k + 1, ns);
48        vstd_extra::arithmetic::lemma_mod_0_add(m.pa_range.start as int, k * ns, ns);
49        vstd_extra::arithmetic::lemma_mod_0_add(m.pa_range.start as int, (k + 1) * ns, ns);
50        vstd_extra::arithmetic::lemma_mod_0_add(m.va_range.start, k * ns, ns);
51        vstd_extra::arithmetic::lemma_mod_0_add(m.va_range.start, (k + 1) * ns, ns);
52
53        assert(sub.inv());
54    }
55
56    /// After `split_if_mapped_huge_spec(new_size)`, a sub-mapping at `cur_va`
57    /// still exists.  The witness is `split_index(m, new_size, k)` where
58    /// `k = (cur_va - m.va_range.start) / new_size`.
59    pub proof fn split_if_mapped_huge_spec_preserves_present(v: Self, new_size: usize)
60        requires
61            v.inv(),
62            v.present(),
63            new_size > 0,
64            v.query_mapping().page_size > 0,
65            v.query_mapping().page_size % new_size == 0,
66        ensures
67            v.split_if_mapped_huge_spec(new_size).present(),
68    {
69        let cur_va = v.cur_va;
70        let m = v.query_mapping();
71        let ps = m.page_size;
72
73        v.lemma_query_mapping();
74
75        let diff: int = cur_va - m.va_range.start;
76        let ki: int = diff / new_size as int;
77        vstd::arithmetic::div_mod::lemma_fundamental_div_mod(diff, new_size as int);
78
79        vstd::arithmetic::div_mod::lemma_fundamental_div_mod(ps as int, new_size as int);
80        assert(ki < ps as int / new_size as int) by {
81            if ki >= ps as int / new_size as int {
82                vstd::arithmetic::mul::lemma_mul_inequality(
83                    ps as int / new_size as int,
84                    ki,
85                    new_size as int,
86                );
87            }
88        };
89
90        let sub = Self::split_index(m, new_size, ki as usize);
91
92        assert(ki * new_size >= 0);
93        assert((ki + 1) * new_size <= ps) by {
94            vstd::arithmetic::mul::lemma_mul_inequality(
95                ki + 1,
96                ps as int / new_size as int,
97                new_size as int,
98            );
99        };
100
101        vstd::arithmetic::mul::lemma_mul_is_distributive_add(new_size as int, ki, 1 as int);
102
103        let new_self = v.split_if_mapped_huge_spec(new_size);
104        let domain = Set::<int>::range(0int, ps as int / new_size as int);
105        assert(domain.contains(ki));
106
107        let new_filter = new_self.mappings.filter(
108            |m2: Mapping| m2.va_range.start <= new_self.cur_va < m2.va_range.end,
109        );
110        vstd::set::lemma_set_contains_len(new_filter, sub);
111    }
112
113    /// After `split_if_mapped_huge_spec(new_size)` on a valid view, the
114    /// mapping at `cur_va` has `page_size == new_size < m.page_size`.
115    ///
116    /// The sub-mapping `split_index(m, new_size, k)` has `page_size = new_size`.
117    /// No other mapping from the original view covers `cur_va` (non-overlapping),
118    /// so `query_mapping()` must return a sub-mapping with `page_size = new_size`.
119    pub proof fn split_if_mapped_huge_spec_decreases_page_size(v: Self, new_size: usize)
120        requires
121            v.inv(),
122            v.present(),
123            new_size > 0,
124            v.query_mapping().page_size > new_size,
125            v.query_mapping().page_size % new_size == 0,
126        ensures
127            v.split_if_mapped_huge_spec(new_size).present(),
128            v.split_if_mapped_huge_spec(new_size).query_mapping().page_size
129                < v.query_mapping().page_size,
130    {
131        Self::split_if_mapped_huge_spec_preserves_present(v, new_size);
132
133        let cur_va = v.cur_va;
134        let m = v.query_mapping();
135        let new_self = v.split_if_mapped_huge_spec(new_size);
136        let m2 = new_self.query_mapping();
137        let ps = m.page_size;
138
139        v.lemma_query_mapping();
140
141        assert(new_self.mappings.contains(m2) && m2.va_range.start <= cur_va && cur_va
142            < m2.va_range.end) by {
143            let f = new_self.mappings.filter(
144                |m3: Mapping| m3.va_range.start <= new_self.cur_va < m3.va_range.end,
145            );
146            vstd::set::lemma_set_choose_len(f);
147        };
148
149        if v.mappings.contains(m2) && m2 != m {
150            assert(false);
151        }
152        let new_mappings = Set::<int>::range(0int, ps as int / new_size as int).map(
153            |n: int| Self::split_index(m, new_size, n as usize),
154        );
155        let k = choose|k: int|
156            0 <= k < ps as int / new_size as int && #[trigger] Self::split_index(
157                m,
158                new_size,
159                k as usize,
160            ) == m2;
161    }
162
163    /// `split_if_mapped_huge_spec` preserves `CursorView::inv()`.
164    ///
165    /// Requires: `v.inv()`, `v.present()`, the mapping at `cur_va` has
166    /// `page_size > new_size`, `page_size % new_size == 0`, and `new_size`
167    /// is itself a valid page size.
168    #[verifier::rlimit(80)]
169    #[verifier::spinoff_prover]
170    pub proof fn split_if_mapped_huge_spec_preserves_inv(v: Self, new_size: usize)
171        requires
172            v.inv(),
173            v.present(),
174            new_size > 0,
175            v.query_mapping().page_size > new_size,
176            v.query_mapping().page_size % new_size == 0,
177            set![4096usize, 2097152, 1073741824].contains(new_size),
178        ensures
179            v.split_if_mapped_huge_spec(new_size).inv(),
180    {
181        let cur_va = v.cur_va;
182        let m = v.query_mapping();
183        let ps = m.page_size;
184        let ns: int = new_size as int;
185        let count: int = ps as int / ns;
186
187        // Establish that m is in v.mappings and covers cur_va.
188        v.lemma_query_mapping();
189        assert(m.va_range.start % new_size as int == 0) by {
190            vstd::arithmetic::mul::lemma_mul_is_commutative(count, ns);
191            vstd::arithmetic::div_mod::lemma_mod_mod(m.va_range.start as int, ns, count);
192        };
193
194        let domain = Set::<int>::range(0int, count);
195        let new_mappings = domain.map(|n: int| Self::split_index(m, new_size, n as usize));
196        let new_self = v.split_if_mapped_huge_spec(new_size);
197
198        assert forall|m2: Mapping| #[trigger] new_self.mappings.contains(m2) implies m2.inv() by {
199            if v.mappings.contains(m2) && m2 != m {
200            } else {
201                let k = choose|k: int|
202                    0 <= k < count && #[trigger] Self::split_index(m, new_size, k as usize) == m2;
203                Self::lemma_split_index_inv(m, new_size, k);
204            }
205        };
206
207        assert forall|m2: Mapping| #[trigger] new_self.mappings.contains(m2) implies {
208            &&& page_table_managed_start_spec::<C>() <= m2.va_range.start
209            &&& m2.va_range.end <= page_table_managed_end_spec::<C>()
210        } by {
211            if v.mappings.contains(m2) && m2 != m {
212            } else {
213                let k = choose|k: int|
214                    0 <= k < count && #[trigger] Self::split_index(m, new_size, k as usize) == m2;
215                Self::lemma_split_index_inv(m, new_size, k);
216            }
217        };
218    }
219
220    /// `split_while_huge` only modifies `mappings`, not `cur_va`.
221    pub broadcast proof fn lemma_split_while_huge_preserves_cur_va(self, size: usize)
222        requires
223            self.inv(),
224            size >= PAGE_SIZE,
225        ensures
226            #[trigger] self.split_while_huge(size).cur_va == self.cur_va,
227        decreases
228                if self.present() {
229                    self.query_mapping().page_size as int
230                } else {
231                    0
232                },
233    {
234        if self.present() {
235            let m = self.query_mapping();
236            if m.page_size > size {
237                let new_size = m.page_size / NR_ENTRIES;
238                let new_self = self.split_if_mapped_huge_spec(new_size);
239                // Establish m.inv() first.
240                self.lemma_query_mapping();
241                // new_size is a valid page size (case split on m.page_size).
242                assert(set![4096usize, 2097152, 1073741824].contains(new_size)) by {
243                    if m.page_size != 2097152 && m.page_size != 1073741824 {
244                        assert(false);
245                    }
246                };
247                Self::split_if_mapped_huge_spec_preserves_inv(self, new_size);
248
249                Self::split_if_mapped_huge_spec_decreases_page_size(self, new_size);
250                Self::lemma_split_while_huge_preserves_cur_va(new_self, size);
251            }
252        }
253    }
254
255    /// `split_while_huge` preserves `CursorView::inv()`.
256    pub proof fn lemma_split_while_huge_preserves_inv(self, size: usize)
257        requires
258            self.inv(),
259            size >= PAGE_SIZE,
260        ensures
261            self.split_while_huge(size).inv(),
262        decreases
263                if self.present() {
264                    self.query_mapping().page_size as int
265                } else {
266                    0
267                },
268    {
269        if self.present() {
270            let m = self.query_mapping();
271            if m.page_size > size {
272                let new_size = m.page_size / NR_ENTRIES;
273                let new_self = self.split_if_mapped_huge_spec(new_size);
274                // Establish m.inv() and call preserves_inv.
275                self.lemma_query_mapping();
276                assert(set![4096usize, 2097152, 1073741824].contains(new_size)) by {
277                    if m.page_size != 2097152 && m.page_size != 1073741824 {
278                        assert(false);
279                    }
280                };
281                Self::split_if_mapped_huge_spec_preserves_inv(self, new_size);
282                Self::split_if_mapped_huge_spec_decreases_page_size(self, new_size);
283                new_self.lemma_split_while_huge_preserves_inv(size);
284            }
285        }
286    }
287
288    /// Composition law for `split_while_huge`:
289    /// splitting to a finer target `s2 <= s1` is the same as first splitting to `s1` and then
290    /// further splitting to `s2`.
291    pub proof fn lemma_split_while_huge_compose(self, s1: usize, s2: usize)
292        requires
293            self.inv(),
294            s1 >= PAGE_SIZE,
295            s2 <= s1,
296        ensures
297            self.split_while_huge(s2) == self.split_while_huge(s1).split_while_huge(s2),
298        decreases
299                if self.present() {
300                    self.query_mapping().page_size as int
301                } else {
302                    0
303                },
304    {
305        if !self.present() {
306            return;
307        }
308        let m = self.query_mapping();
309        if m.page_size <= s1 {
310            return;
311        }
312        let new_size = m.page_size / NR_ENTRIES;
313        self.lemma_query_mapping();
314        assert(set![4096usize, 2097152, 1073741824].contains(new_size) && m.page_size % new_size
315            == 0) by {
316            if m.page_size == 2097152 {
317                assert(2097152usize % (2097152usize / 512usize) == 0) by (compute_only);
318            } else {
319                assert(1073741824usize % (1073741824usize / 512usize) == 0) by (compute_only);
320            }
321        };
322        Self::split_if_mapped_huge_spec_preserves_inv(self, new_size);
323        Self::split_if_mapped_huge_spec_decreases_page_size(self, new_size);
324        self.split_if_mapped_huge_spec(new_size).lemma_split_while_huge_compose(s1, s2);
325    }
326
327    /// When `split_while_huge(size)` is a no-op and the view is `present()`,
328    /// the mapping at `cur_va` already has `page_size <= size`.
329    pub proof fn split_while_huge_noop_implies_page_size_le(self, size: usize)
330        requires
331            self.inv(),
332            size >= PAGE_SIZE,
333            self.split_while_huge(size) == self,
334            self.present(),
335        ensures
336            self.query_mapping().page_size <= size,
337    {
338        let m = self.query_mapping();
339        if m.page_size > size {
340            let new_size = m.page_size / NR_ENTRIES;
341            self.lemma_query_mapping();
342            assert(set![4096usize, 2097152, 1073741824].contains(new_size)) by {
343                if m.page_size == 2097152 {
344                } else if m.page_size == 1073741824 {
345                } else {
346                    assert(false);
347                }
348            };
349            Self::split_if_mapped_huge_spec_preserves_inv(self, new_size);
350            let new_self = self.split_if_mapped_huge_spec(new_size);
351            new_self.split_while_huge_refinement(size, m);
352            let p = choose|p: Mapping| #[trigger]
353                new_self.mappings.contains(p) && p.va_range.start <= m.va_range.start
354                    && m.va_range.end <= p.va_range.end && m.pa_range.start == (p.pa_range.start + (
355                m.va_range.start - p.va_range.start)) as Paddr && m.property == p.property;
356            if self.mappings.contains(p) {
357            } else {
358                let new_mappings = Set::<int>::range(
359                    0int,
360                    m.page_size as int / new_size as int,
361                ).map(|n: int| Self::split_index(m, new_size, n as usize));
362                let k = choose|k: int|
363                    0 <= k < m.page_size as int / new_size as int && #[trigger] Self::split_index(
364                        m,
365                        new_size,
366                        k as usize,
367                    ) == p;
368            }
369        }
370    }
371
372    /// When the mapping at `cur_va` is exactly one split-step above `size`
373    /// (i.e. `query_mapping().page_size / NR_ENTRIES == size`), one step of
374    /// `split_while_huge` equals `split_if_mapped_huge_spec`:
375    ///
376    /// `self.split_while_huge(size) == self.split_if_mapped_huge_spec(size)`
377    ///
378    /// This is because `split_while_huge` takes one step
379    /// `split_if_mapped_huge_spec(m.page_size / NR_ENTRIES)` = `split_if_mapped_huge_spec(size)`,
380    /// then the sub-mapping at `cur_va` has `page_size == size <= size`, so it stops.
381    pub proof fn split_while_huge_one_step(self, size: usize)
382        requires
383            self.inv(),
384            self.present(),
385            self.query_mapping().page_size > size,
386            self.query_mapping().page_size / NR_ENTRIES == size,
387            self.query_mapping().page_size % size == 0,
388            set![4096usize, 2097152, 1073741824].contains(size),
389        ensures
390            self.split_while_huge(size).mappings == self.split_if_mapped_huge_spec(size).mappings,
391    {
392        let m = self.query_mapping();
393        let new_size = m.page_size / NR_ENTRIES;
394        self.lemma_query_mapping();
395        Self::split_if_mapped_huge_spec_preserves_inv(self, new_size);
396        Self::split_if_mapped_huge_spec_decreases_page_size(self, new_size);
397        let new_self = self.split_if_mapped_huge_spec(new_size);
398
399        assert(new_self.query_mapping().page_size == new_size) by {
400            let new_m = new_self.query_mapping();
401            new_self.lemma_query_mapping();
402            if self.mappings.contains(new_m) && new_m != m {
403                assert(false);
404            }
405            let new_mappings = Set::<int>::range(0int, m.page_size as int / new_size as int).map(
406                |n: int| Self::split_index(m, new_size, n as usize),
407            );
408        };
409        assert(new_self.split_while_huge(size) == new_self);
410    }
411
412    /// Locality of `split_while_huge`: a mapping `m2` that is in `self.mappings`
413    /// and whose VA range does not contain `cur_va` is preserved.
414    #[verifier::rlimit(80)]
415    pub proof fn split_while_huge_locality(self, size: usize, m2: Mapping)
416        requires
417            self.inv(),
418            size >= PAGE_SIZE,
419            self.mappings.contains(m2),
420            !(m2.va_range.start <= self.cur_va < m2.va_range.end),
421        ensures
422            self.split_while_huge(size).mappings.contains(m2),
423        decreases
424                if self.present() {
425                    self.query_mapping().page_size as int
426                } else {
427                    0
428                },
429    {
430        if self.present() {
431            let m = self.query_mapping();
432            if m.page_size > size {
433                let new_size = m.page_size / NR_ENTRIES;
434                // Establish m covers cur_va.
435                self.lemma_query_mapping();
436                // m2 != m and disjoint va_ranges (non-overlap invariant).
437                assert(set![4096usize, 2097152, 1073741824].contains(new_size)) by {
438                    if m.page_size != 2097152 && m.page_size != 1073741824 {
439                        assert(false);
440                    }
441                };
442                let new_self = self.split_if_mapped_huge_spec(new_size);
443                Self::split_if_mapped_huge_spec_preserves_inv(self, new_size);
444                Self::split_if_mapped_huge_spec_decreases_page_size(self, new_size);
445                new_self.split_while_huge_locality(size, m2);
446            }
447        }
448    }
449
450    /// Refinement: every mapping in `split_while_huge(size).mappings` is either
451    /// from `self.mappings` or a sub-mapping of an entry in `self.mappings`.
452    /// Base lemma: every mapping in `split_if_mapped_huge_spec(new_size).mappings`
453    /// is either from the original mappings or a sub-mapping of `query_mapping()`.
454    pub proof fn split_if_mapped_huge_spec_refinement(self, new_size: usize, e: Mapping)
455        requires
456            self.inv(),
457            self.present(),
458            new_size > 0,
459            self.query_mapping().page_size > new_size,
460            self.query_mapping().page_size % new_size == 0,
461            self.split_if_mapped_huge_spec(new_size).mappings.contains(e),
462        ensures
463            self.mappings.contains(e) || {
464                let parent = self.query_mapping();
465                &&& self.mappings.contains(parent)
466                &&& parent.va_range.start <= e.va_range.start
467                &&& e.va_range.end <= parent.va_range.end
468                &&& e.pa_range.start == (parent.pa_range.start + (e.va_range.start
469                    - parent.va_range.start)) as Paddr
470                &&& e.property == parent.property
471            },
472    {
473        let qm = self.query_mapping();
474        let ps = qm.page_size;
475        let ns: int = new_size as int;
476        let count: int = ps as int / ns;
477        let new_self = self.split_if_mapped_huge_spec(new_size);
478        let domain = Set::<int>::range(0int, count);
479        let new_mappings = domain.map(|n: int| Self::split_index(qm, new_size, n as usize));
480
481        // Establish qm ∈ self.mappings.
482        self.lemma_query_mapping();
483
484        if self.mappings.remove(qm).contains(e) {
485        } else {
486            assert(new_mappings.contains(e));
487            let k = choose|k: int|
488                0 <= k < count && #[trigger] Self::split_index(qm, new_size, k as usize) == e;
489
490            vstd::arithmetic::div_mod::lemma_fundamental_div_mod(ps as int, ns);
491            vstd::arithmetic::div_mod::lemma_div_nonincreasing(ps as int, ns);
492
493            vstd::arithmetic::mul::lemma_mul_inequality(k + 1, count, ns);
494        }
495    }
496
497    pub proof fn split_while_huge_refinement(self, size: usize, m: Mapping)
498        requires
499            self.inv(),
500            size >= PAGE_SIZE,
501            self.split_while_huge(size).mappings.contains(m),
502        ensures
503            self.mappings.contains(m) || exists|parent: Mapping| #[trigger]
504                self.mappings.contains(parent) && parent.va_range.start <= m.va_range.start
505                    && m.va_range.end <= parent.va_range.end && m.pa_range.start == (
506                parent.pa_range.start + (m.va_range.start - parent.va_range.start)) as Paddr
507                    && m.property == parent.property,
508        decreases
509                if self.present() {
510                    self.query_mapping().page_size as int
511                } else {
512                    0
513                },
514    {
515        if self.present() {
516            let qm = self.query_mapping();
517            if qm.page_size > size {
518                let new_size = qm.page_size / NR_ENTRIES;
519                let new_self = self.split_if_mapped_huge_spec(new_size);
520
521                self.lemma_query_mapping();
522                assert(self.mappings.filter(
523                    |m2: Mapping| m2.va_range.start <= self.cur_va < m2.va_range.end,
524                ).contains(qm));
525                assert(set![4096usize, 2097152, 1073741824].contains(new_size)) by {
526                    if qm.page_size != 2097152 && qm.page_size != 1073741824 {
527                        assert(false);
528                    }
529                };
530                Self::split_if_mapped_huge_spec_preserves_inv(self, new_size);
531                Self::split_if_mapped_huge_spec_decreases_page_size(self, new_size);
532
533                new_self.split_while_huge_refinement(size, m);
534                new_self.lemma_split_while_huge_preserves_inv(size);
535
536                if new_self.mappings.contains(m) {
537                    self.split_if_mapped_huge_spec_refinement(new_size, m);
538                } else {
539                    let p = choose|p: Mapping| #[trigger]
540                        new_self.mappings.contains(p) && p.va_range.start <= m.va_range.start
541                            && m.va_range.end <= p.va_range.end && m.pa_range.start == (
542                        p.pa_range.start + (m.va_range.start - p.va_range.start)) as Paddr
543                            && m.property == p.property;
544                    self.split_if_mapped_huge_spec_refinement(new_size, p);
545                    if !self.mappings.contains(p) {
546                        assert(exists|parent: Mapping| #[trigger]
547                            self.mappings.contains(parent) && parent.va_range.start
548                                <= m.va_range.start && m.va_range.end <= parent.va_range.end
549                                && m.pa_range.start == (parent.pa_range.start + (m.va_range.start
550                                - parent.va_range.start)) as Paddr && m.property == parent.property)
551                            by {
552                            let parent = qm;
553                        }
554                    } else {
555                        assert(exists|parent: Mapping| #[trigger]
556                            self.mappings.contains(parent) && parent.va_range.start
557                                <= m.va_range.start && m.va_range.end <= parent.va_range.end
558                                && m.pa_range.start == (parent.pa_range.start + (m.va_range.start
559                                - parent.va_range.start)) as Paddr && m.property == parent.property)
560                            by {
561                            let parent = p;
562                        }
563                    }
564                }
565            }
566        }
567    }
568
569    /// `split_while_huge` produces a set disjoint from any set that is
570    /// pairwise VA-disjoint from `self.mappings`.
571    ///
572    /// Set-disjointness of `other` from `self.mappings` is **not** sufficient
573    /// (counterexample: `other = {split_index(m, k, 0)}` collides with the
574    /// first sub-mapping after one split step). We need VA-disjointness so
575    /// that sub-mappings — which lie strictly inside the parent's va_range
576    /// and hence have distinct va_ranges from anything in `other` — cannot
577    /// equal any element of `other`.
578    pub proof fn split_while_huge_disjoint(self, size: usize, other: Set<Mapping>)
579        requires
580            self.inv(),
581            size >= PAGE_SIZE,
582            forall|m: Mapping, x: Mapping| #[trigger]
583                self.mappings.contains(m) && #[trigger] other.contains(x)
584                    ==> Mapping::disjoint_vaddrs(m, x),
585        ensures
586            self.split_while_huge(size).mappings.disjoint(other),
587        decreases
588                if self.present() {
589                    self.query_mapping().page_size as int
590                } else {
591                    0
592                },
593    {
594        if !self.present() {
595            // split_while_huge is a no-op; disjointness is by va-disjoint hypothesis.
596            assert forall|x: Mapping|
597                #![trigger other.contains(x)]
598                other.contains(x) implies !self.split_while_huge(size).mappings.contains(x) by {
599                if self.mappings.contains(x) {
600                    assert(x.inv());
601                }
602            };
603            return;
604        }
605        let m = self.query_mapping();
606        if m.page_size <= size {
607            assert forall|x: Mapping|
608                #![trigger other.contains(x)]
609                other.contains(x) implies !self.split_while_huge(size).mappings.contains(x) by {
610                if self.mappings.contains(x) {
611                    assert(x.inv());
612                }
613            };
614            return;
615        }
616        let new_size = m.page_size / NR_ENTRIES;
617
618        // Standard scaffolding: m ∈ self.mappings, m covers cur_va, m.inv().
619        self.lemma_query_mapping();
620
621        assert(set![4096usize, 2097152, 1073741824].contains(new_size)) by {
622            if m.page_size == 2097152 {
623            } else if m.page_size == 1073741824 {
624            } else {
625                assert(false);
626            }
627        };
628        assert(m.page_size % new_size == 0) by {
629            assert(2097152usize % (2097152usize / 512usize) == 0) by (compute_only);
630            assert(1073741824usize % (1073741824usize / 512usize) == 0) by (compute_only);
631        };
632        assert(m.page_size > new_size) by {
633            assert(2097152usize > 2097152usize / 512usize) by (compute_only);
634            assert(1073741824usize > 1073741824usize / 512usize) by (compute_only);
635        };
636        Self::split_if_mapped_huge_spec_preserves_inv(self, new_size);
637        Self::split_if_mapped_huge_spec_decreases_page_size(self, new_size);
638        let new_self = self.split_if_mapped_huge_spec(new_size);
639
640        // Recursive call: establish va-disjoint hypothesis for new_self.
641        assert forall|m2: Mapping, x: Mapping| #[trigger]
642            new_self.mappings.contains(m2) && #[trigger] other.contains(
643                x,
644            ) implies Mapping::disjoint_vaddrs(m2, x) by {
645            if self.mappings.contains(m2) {
646                // Existing mapping preserved by split: va-disjoint by hypothesis.
647            } else {
648                // m2 is a sub-mapping of m, so its va_range is contained in m.va_range,
649                // and disjointness from x follows from disjointness of m and x.
650                Self::split_if_mapped_huge_spec_refinement(self, new_size, m2);
651                assert(Mapping::disjoint_vaddrs(m, x));
652            }
653        };
654
655        new_self.split_while_huge_disjoint(size, other);
656    }
657}
658
659impl<'rcu, C: PageTableConfig> CursorOwner<'rcu, C> {
660    /// When the current entry is a PT node at level `self.level`, any mapping at `cur_va` has
661    /// `page_size <= page_size(self.level - 1)`.  Therefore `split_while_huge` at
662    /// `page_size(self.level - 1)` does not split anything and is a no-op on the abstract view.
663    /// When present, the query_mapping is from the current subtree's view_rec.
664    pub proof fn query_mapping_from_subtree(self, qm: Mapping)
665        requires
666            self.inv(),
667            self.in_barrier_va(),
668            self@.inv(),
669            self@.present(),
670            qm == self@.query_mapping(),
671        ensures
672            PageTableOwner(self.cur_subtree()).view_rec(self.cur_subtree().value().path).contains(
673                qm,
674            ),
675    {
676        self@.lemma_query_mapping();
677        self.mapping_covering_cur_va_from_cur_subtree(qm);
678    }
679
680    pub proof fn split_while_huge_node_noop(self)
681        requires
682            self.inv(),
683            self.in_barrier_va(),
684            self.cur_entry_owner().is_node(),
685            self.level > 1,
686        ensures
687            self@.split_while_huge(page_size::<PagingConsts>((self.level - 1) as PagingLevel))
688                == self@,
689    {
690        self.view_preserves_inv();
691        if self@.present() {
692            let subtree = self.cur_subtree();
693            let path = subtree.value().path;
694            let qm = self@.query_mapping();
695            self.query_mapping_from_subtree(qm);
696            PageTableOwner(subtree).lemma_view_rec_node_page_size_bound(path, qm);
697        }
698    }
699
700    /// When the current entry is absent, there is no mapping at `cur_va` in the abstract view,
701    /// so `split_while_huge` finds nothing to split and is a no-op for any target size.
702    pub proof fn split_while_huge_absent_noop(self, size: usize)
703        requires
704            self.inv(),
705            self.in_barrier_va(),
706            self.cur_entry_owner().is_absent(),
707        ensures
708            self@.split_while_huge(size) == self@,
709    {
710        self.view_preserves_inv();
711        self.lemma_cur_entry_absent_not_present();
712    }
713
714    pub proof fn lemma_split_while_huge_at_level_noop(self)
715        requires
716            self.inv(),
717            self.in_barrier_va(),
718        ensures
719            self@.split_while_huge(page_size::<PagingConsts>(self.level as PagingLevel)) == self@,
720    {
721        self.view_preserves_inv();
722        if self@.present() {
723            self.lemma_cur_subtree_inv();
724            let subtree = self.cur_subtree();
725            let path = subtree.value().path;
726            let qm = self@.query_mapping();
727            self.query_mapping_from_subtree(qm);
728            PageTableOwner(subtree).lemma_view_rec_page_size_bound(path, qm);
729        }
730    }
731
732    /// After split_if_mapped_huge + push_level, the mappings equal
733    /// `old_view.split_while_huge(page_size(current_level))`.
734    pub proof fn find_next_split_push_equals_split_while_huge(self, old_view: CursorView<C>)
735        requires
736            self.inv(),
737            old_view.inv(),
738            self.cur_entry_owner().is_frame(),
739            self@.cur_va == old_view.cur_va,
740            old_view.present(),
741            old_view.query_mapping().page_size > page_size::<PagingConsts>(
742                self.level as PagingLevel,
743            ),
744            old_view.query_mapping().page_size / NR_ENTRIES == page_size::<PagingConsts>(
745                self.level as PagingLevel,
746            ),
747            old_view.query_mapping().page_size % page_size::<PagingConsts>(
748                self.level as PagingLevel,
749            ) == 0,
750            self@.mappings =~= old_view.split_if_mapped_huge_spec(
751                page_size::<PagingConsts>(self.level as PagingLevel),
752            ).mappings,
753        ensures
754            self@ == old_view.split_while_huge(
755                page_size::<PagingConsts>(self.level as PagingLevel),
756            ),
757    {
758        let ps = page_size::<PagingConsts>(self.level as PagingLevel);
759        let m = old_view.query_mapping();
760        let f = old_view.mappings.filter(
761            |m2: Mapping| m2.va_range.start <= old_view.cur_va < m2.va_range.end,
762        );
763        crate::specs::mm::page_table::cursor::page_size_lemmas::lemma_page_size_spec_values();
764        old_view.split_while_huge_one_step(ps);
765        old_view.lemma_split_while_huge_preserves_cur_va(ps);
766    }
767}
768
769} // verus!
ostd/specs/mm/page_table/cursor/split_while_huge_lemmas.rs

ostd/specs/mm/page_table/cursor/
split_while_huge_lemmas.rs
