ostd/mm/frame/meta/
mapping.rs

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

ostd/mm/frame/meta/
mapping.rs
