ostd/mm/frame/meta/
mapping.rs

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

ostd/mm/frame/meta/
mapping.rs
