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

ostd/specs/mm/page_table/
mapping_set_lemmas.rs
