ostd/specs/mm/page_table/
mapping_set_lemmas.rs

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

ostd/specs/mm/page_table/
mapping_set_lemmas.rs
