ostd/specs/mm/page_table/
mapping_set_lemmas.rs

1use vstd::prelude::*;
2use vstd::set_lib::*;
3
4use crate::mm::{MAX_USERSPACE_VADDR, Vaddr};
5use crate::specs::arch::{MAX_PADDR, PAGE_SIZE};
6
7use super::view::Mapping;
8
9verus! {
10
11/// Well-formed mapping set: all inv(), pairwise VA-disjoint.
12pub open spec fn wf_mapping_set(s: Set<Mapping>) -> bool {
13    &&& forall|m: Mapping| #![auto] s.contains(m) ==> m.inv()
14    &&& forall|m: Mapping, n: Mapping|
15        #![auto]
16        s.contains(m) && s.contains(n) && m != n ==> m.va_range.end <= n.va_range.start
17            || n.va_range.end <= m.va_range.start
18}
19
20/// A well-formed mapping set whose VA ranges all lie within `[lo, hi)` has
21/// cardinality at most `(hi - lo) / PAGE_SIZE`.
22///
23/// Proof by induction on `|s|`: pick any element `m`, partition the rest into
24/// mappings below `m` and mappings above `m`, recurse on each half.
25pub proof fn lemma_mapping_set_cardinality_in_range(s: Set<Mapping>, lo: int, hi: int)
26    requires
27        wf_mapping_set(s),
28        forall|m: Mapping| #[trigger]
29            s.contains(m) ==> lo <= m.va_range.start && m.va_range.end <= hi,
30        lo <= hi,
31    ensures
32        s.len() * PAGE_SIZE <= hi - lo,
33    decreases s.len(),
34{
35    if s.len() != 0 {
36        let m = s.choose();
37        let rest = s.remove(m);
38        vstd::set::lemma_set_remove_len(s, m);
39        assert(m.inv());
40
41        let below = rest.filter(|n: Mapping| n.va_range.end <= m.va_range.start);
42        let above = rest.filter(|n: Mapping| n.va_range.start >= m.va_range.end);
43
44        assert(rest == below.union(above)) by {
45            assert forall|n: Mapping| rest.contains(n) implies below.contains(n) || above.contains(
46                n,
47            ) by {
48                assert(s.contains(n) && n != m);
49            };
50        };
51
52        assert(below.disjoint(above)) by {
53            assert forall|n: Mapping| below.contains(n) implies !above.contains(n) by {
54                if above.contains(n) {
55                    assert(n.inv());
56                }
57            };
58        };
59
60        vstd::set_lib::lemma_set_disjoint_lens(below, above);
61        assert(rest.len() == below.len() + above.len());
62
63        assert(wf_mapping_set(below)) by {
64            assert forall|a: Mapping, b: Mapping| #[trigger]
65                below.contains(a) && #[trigger] below.contains(b) && a != b implies a.va_range.end
66                <= b.va_range.start || b.va_range.end <= a.va_range.start by {};
67        };
68        assert(wf_mapping_set(above)) by {
69            assert forall|a: Mapping, b: Mapping| #[trigger]
70                above.contains(a) && #[trigger] above.contains(b) && a != b implies a.va_range.end
71                <= b.va_range.start || b.va_range.end <= a.va_range.start by {};
72        };
73
74        lemma_mapping_set_cardinality_in_range(below, lo, m.va_range.start);
75        lemma_mapping_set_cardinality_in_range(above, m.va_range.end, hi);
76
77        vstd::arithmetic::mul::lemma_mul_is_distributive_add(
78            PAGE_SIZE as int,
79            (below.len() + above.len()) as int,
80            1,
81        );
82        vstd::arithmetic::mul::lemma_mul_is_distributive_add(
83            PAGE_SIZE as int,
84            below.len() as int,
85            above.len() as int,
86        );
87    }
88}
89
90/// **Main lemma**: A well-formed mapping set has cardinality at most
91/// `bound / PAGE_SIZE`, where `bound` is its largest element.
92pub proof fn lemma_mapping_set_cardinality_bound(s: Set<Mapping>, bound: usize)
93    requires
94        wf_mapping_set(s),
95        forall|m: Mapping| #[trigger]
96            s.contains(m) ==> 0 <= m.va_range.start && m.va_range.end <= bound,
97    ensures
98        s.len() <= bound / PAGE_SIZE,
99{
100    lemma_mapping_set_cardinality_in_range(s, 0, bound as int);
101    vstd::arithmetic::div_mod::lemma_fundamental_div_mod(bound as int, PAGE_SIZE as int);
102    vstd::arithmetic::div_mod::lemma_div_pos_is_pos(bound as int, PAGE_SIZE as int);
103    if s.len() > bound / PAGE_SIZE {
104        vstd::arithmetic::mul::lemma_mul_inequality(
105            bound as int / PAGE_SIZE as int + 1,
106            s.len() as int,
107            PAGE_SIZE as int,
108        );
109        vstd::arithmetic::mul::lemma_mul_is_distributive_add(
110            PAGE_SIZE as int,
111            bound as int / PAGE_SIZE as int,
112            1,
113        );
114    }
115}
116
117/// Corollary: the cardinality fits in usize.
118///
119/// The bound `0x0000_8000_0000_0000` (= 2^47) is the new upper end derived
120/// from `vaddr_range_bounds_spec::<UserPtConfig>` — one page looser than
121/// the old `MAX_USERSPACE_VADDR`, but still gives a comfortable
122/// `2^35 < usize::MAX`.
123pub proof fn lemma_mapping_set_cardinality_fits_usize(s: Set<Mapping>)
124    requires
125        wf_mapping_set(s),
126        forall|m: Mapping| #[trigger]
127            s.contains(m) ==> m.va_range.end <= 0x0000_8000_0000_0000_usize,
128    ensures
129        s.len() < usize::MAX,
130{
131    // `0 <= m.va_range.start` follows from `wf_mapping_set(s)` ⇒ `m.inv()`,
132    // which has `0 <= m.va_range.start`.
133    assert forall|m: Mapping| #[trigger] s.contains(m) implies 0 <= m.va_range.start
134        && m.va_range.end <= 0x0000_8000_0000_0000_usize by {
135        assert(m.inv());
136    };
137    lemma_mapping_set_cardinality_bound(s, 0x0000_8000_0000_0000_usize);
138    assert(0x0000_8000_0000_0000_usize / PAGE_SIZE < usize::MAX) by (compute_only);
139}
140
141/// A subset of a wf_mapping_set is also wf.
142pub proof fn lemma_wf_subset(s: Set<Mapping>, sub: Set<Mapping>)
143    requires
144        wf_mapping_set(s),
145        sub.subset_of(s),
146    ensures
147        wf_mapping_set(sub),
148{
149}
150
151/// A union of two wf sets is wf if every element of one is VA-disjoint from every element of the other.
152pub proof fn lemma_wf_union(a: Set<Mapping>, b: Set<Mapping>)
153    requires
154        wf_mapping_set(a),
155        wf_mapping_set(b),
156        forall|m: Mapping, n: Mapping| #[trigger]
157            a.contains(m) && #[trigger] b.contains(n) ==> m.va_range.end <= n.va_range.start
158                || n.va_range.end <= m.va_range.start,
159    ensures
160        wf_mapping_set(a.union(b)),
161{
162}
163
164/// If `m` is a sub-mapping of `p` and `p` is a sub-mapping of `orig`,
165/// then `m` is a sub-mapping of `orig` (PA arithmetic composes).
166pub proof fn lemma_sub_mapping_pa_compose(m: Mapping, p: Mapping, orig: Mapping)
167    requires
168        m.inv(),
169        orig.inv(),
170        p.va_range.start >= orig.va_range.start,
171        p.va_range.end <= orig.va_range.end,
172        p.pa_range.start == (orig.pa_range.start + (p.va_range.start
173            - orig.va_range.start)) as usize,
174        p.property == orig.property,
175        m.va_range.start >= p.va_range.start,
176        m.va_range.end <= p.va_range.end,
177        m.pa_range.start == (p.pa_range.start + (m.va_range.start - p.va_range.start)) as usize,
178        m.property == p.property,
179    ensures
180        orig.va_range.start <= m.va_range.start,
181        m.va_range.end <= orig.va_range.end,
182        m.pa_range.start == (orig.pa_range.start + (m.va_range.start
183            - orig.va_range.start)) as usize,
184        m.property == orig.property,
185{
186    assert(MAX_PADDR < usize::MAX) by (compute_only);
187}
188
189} // verus!
ostd/specs/mm/page_table/mapping_set_lemmas.rs

ostd/specs/mm/page_table/
mapping_set_lemmas.rs
