ostd/specs/mm/page_table/
mapping_set_lemmas.rs

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

ostd/specs/mm/page_table/
mapping_set_lemmas.rs
