ostd/specs/mm/frame/
mapping.rs

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

ostd/specs/mm/frame/
mapping.rs
