ostd/specs/mm/page_table/
mapping_set_lemmas.rs

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

ostd/specs/mm/page_table/
mapping_set_lemmas.rs
