ostd/specs/mm/page_table/
mapping_set_lemmas.rs

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

ostd/specs/mm/page_table/
mapping_set_lemmas.rs
