ostd/specs/mm/frame/
mapping.rs

1use vstd::prelude::*;
2use vstd_extra::extern_const::*;
3
4use super::*;
5
6use core::mem::size_of;
7use core::ops::Range;
8
9use crate::mm::frame::meta::{lemma_meta_slot_size, meta_slot_size};
10use crate::mm::frame::MetaSlot;
11use crate::mm::{Paddr, Vaddr};
12use crate::specs::arch::kspace::FRAME_METADATA_RANGE;
13use crate::specs::arch::mm::{MAX_NR_PAGES, MAX_PADDR, PAGE_SIZE};
14
15verus! {
16
17extern_const!(
18/// Metaslot size.
19pub META_SLOT_SIZE [META_SLOT_SIZE_SPEC, CONST_META_SLOT_SIZE]: usize = 64
20);
21
22pub open spec fn max_meta_slots() -> int {
23    (FRAME_METADATA_RANGE().end - FRAME_METADATA_RANGE().start) / META_SLOT_SIZE() as int
24}
25
26pub open spec fn meta_addr(i: usize) -> (res: usize)
27    recommends
28        0 <= i < max_meta_slots() as usize,
29{
30    (FRAME_METADATA_RANGE().start + i * META_SLOT_SIZE()) as usize
31}
32
33#[allow(non_snake_case)]
34pub broadcast proof fn lemma_FRAME_METADATA_RANGE_is_page_aligned()
35    ensures
36        #[trigger] FRAME_METADATA_RANGE().start % PAGE_SIZE() == 0,
37        FRAME_METADATA_RANGE().end % PAGE_SIZE() == 0,
38{
39}
40
41#[allow(non_snake_case)]
42pub broadcast proof fn lemma_FRAME_METADATA_RANGE_is_large_enough()
43    ensures
44        #[trigger] FRAME_METADATA_RANGE().end >= FRAME_METADATA_RANGE().start + MAX_NR_PAGES() * META_SLOT_SIZE(),
45{
46}
47
48#[verifier::inline]
49pub open spec fn frame_to_meta_spec(paddr: Paddr) -> (res: Vaddr)
50    recommends
51        paddr % PAGE_SIZE() == 0,
52        paddr < MAX_PADDR(),
53{
54    (FRAME_METADATA_RANGE().start + (paddr / PAGE_SIZE()) * meta_slot_size()) as usize
55}
56
57#[verifier::inline]
58pub open spec fn meta_to_frame_spec(vaddr: Vaddr) -> Paddr
59    recommends
60        vaddr % size_of::<MetaSlot>() == 0,
61        FRAME_METADATA_RANGE().start <= vaddr < FRAME_METADATA_RANGE().end,
62{
63    ((vaddr - FRAME_METADATA_RANGE().start) / META_SLOT_SIZE() as int * PAGE_SIZE()) as usize
64}
65
66#[verifier::inline]
67pub open spec fn frame_to_index_spec(paddr: Paddr) -> usize {
68    paddr / PAGE_SIZE()
69}
70
71#[verifier::inline]
72pub open spec fn index_to_frame_spec(index: usize) -> Paddr {
73    (index * PAGE_SIZE()) as usize
74}
75
76#[verifier::when_used_as_spec(frame_to_index_spec)]
77pub fn frame_to_index(paddr: Paddr) -> (res: usize)
78    requires
79        paddr % PAGE_SIZE() == 0,
80    ensures
81        res == frame_to_index_spec(paddr),
82{
83    paddr / PAGE_SIZE()
84}
85
86#[verifier::when_used_as_spec(index_to_frame_spec)]
87pub fn index_to_frame(index: usize) -> (res: Paddr)
88    requires
89        index < max_meta_slots(),
90    ensures
91        res == index_to_frame_spec(index),
92{
93    index * PAGE_SIZE()
94}
95
96} // verus!
97verus! {
98
99#[inline(always)]
100#[verifier::when_used_as_spec(frame_to_meta_spec)]
101pub fn frame_to_meta(paddr: Paddr) -> (res: Vaddr)
102    requires
103        paddr % PAGE_SIZE() == 0,
104        paddr < MAX_PADDR(),
105    ensures
106        res == frame_to_meta_spec(paddr),
107        res % META_SLOT_SIZE() == 0,
108{
109    let base = FRAME_METADATA_RANGE().start;
110    let offset = paddr / PAGE_SIZE();
111    base + offset * META_SLOT_SIZE()
112}
113
114#[inline(always)]
115#[verifier::when_used_as_spec(meta_to_frame_spec)]
116pub fn meta_to_frame(vaddr: Vaddr) -> (res: Paddr)
117    requires
118        FRAME_METADATA_RANGE().start <= vaddr && vaddr < FRAME_METADATA_RANGE().end,
119        vaddr % META_SLOT_SIZE() == 0,
120    ensures
121        res == meta_to_frame_spec(vaddr),
122        res % PAGE_SIZE() == 0,
123{
124    let base = FRAME_METADATA_RANGE().start;
125    let offset = (vaddr - base) / META_SLOT_SIZE();
126    offset * PAGE_SIZE()
127}
128
129pub broadcast proof fn lemma_paddr_to_meta_biinjective(paddr: Paddr)
130    requires
131        paddr % PAGE_SIZE() == 0,
132        paddr < MAX_PADDR(),
133    ensures
134        #[trigger] meta_to_frame(frame_to_meta(paddr)) == paddr,
135{
136}
137
138pub broadcast proof fn lemma_meta_to_paddr_biinjective(vaddr: Vaddr)
139    requires
140        FRAME_METADATA_RANGE().start <= vaddr && vaddr < FRAME_METADATA_RANGE().end,
141        vaddr % META_SLOT_SIZE() == 0,
142    ensures
143        #[trigger] frame_to_meta(meta_to_frame(vaddr)) == vaddr,
144{
145}
146
147pub broadcast proof fn lemma_meta_to_frame_soundness(meta: Vaddr)
148    requires
149        meta % META_SLOT_SIZE() == 0,
150        FRAME_METADATA_RANGE().start <= meta && meta < FRAME_METADATA_RANGE().start + MAX_NR_PAGES()
151            * META_SLOT_SIZE(),
152    ensures
153        #[trigger] meta_to_frame(meta) % PAGE_SIZE() == 0,
154        meta_to_frame(meta) < MAX_PADDR(),
155{
156}
157
158pub broadcast proof fn lemma_frame_to_meta_soundness(page: Paddr)
159    requires
160        page % PAGE_SIZE() == 0,
161        page < MAX_PADDR(),
162    ensures
163        #[trigger] frame_to_meta(page) % META_SLOT_SIZE() == 0,
164        FRAME_METADATA_RANGE().start <= frame_to_meta(page) && frame_to_meta(page)
165            < FRAME_METADATA_RANGE().start + MAX_NR_PAGES() * META_SLOT_SIZE(),
166{
167}
168
169pub broadcast proof fn lemma_meta_to_frame_alignment(meta: Vaddr)
170    requires
171        meta % META_SLOT_SIZE() == 0,
172        FRAME_METADATA_RANGE().start <= meta && meta < FRAME_METADATA_RANGE().start + MAX_NR_PAGES()
173            * META_SLOT_SIZE(),
174    ensures
175        #[trigger] meta_to_frame(meta) % PAGE_SIZE() == 0,
176        meta_to_frame(meta) < MAX_PADDR(),
177{
178}
179
180pub broadcast group group_page_meta {
181    lemma_meta_slot_size,
182    lemma_FRAME_METADATA_RANGE_is_page_aligned,
183    lemma_FRAME_METADATA_RANGE_is_large_enough,
184    lemma_paddr_to_meta_biinjective,
185    lemma_meta_to_paddr_biinjective,
186    lemma_meta_to_frame_soundness,
187    lemma_frame_to_meta_soundness,
188    lemma_meta_to_frame_alignment,
189}
190
191} // verus!
ostd/specs/mm/frame/mapping.rs

ostd/specs/mm/frame/
mapping.rs
