ostd/specs/mm/frame/
mapping.rs

1use vstd::prelude::*;
2
3use crate::specs::arch::*;
4
5use super::*;
6use crate::mm::{
7    Paddr, Vaddr,
8    frame::meta::{
9        META_SLOT_SIZE, MetaSlot,
10        mapping::{frame_to_meta, meta_to_frame},
11    },
12    kspace::FRAME_METADATA_RANGE,
13};
14use core::{mem::size_of, ops::Range};
15
16verus! {
17
18pub open spec fn max_meta_slots() -> int {
19    (FRAME_METADATA_RANGE.end - FRAME_METADATA_RANGE.start) / META_SLOT_SIZE as int
20}
21
22#[verifier::inline]
23pub open spec fn frame_to_index(paddr: Paddr) -> int
24    recommends
25        paddr % PAGE_SIZE == 0,
26{
27    (paddr / PAGE_SIZE) as int
28}
29
30pub open spec fn index_to_meta(i: int) -> Vaddr
31    recommends
32        0 <= i < max_meta_slots(),
33{
34    (FRAME_METADATA_RANGE.start + i * META_SLOT_SIZE) as Vaddr
35}
36
37/// Converts a frame metadata-slot virtual address to its frame index.
38pub open spec fn meta_to_index(vaddr: Vaddr) -> int {
39    frame_to_index(meta_to_frame(vaddr))
40}
41
42#[verifier::inline]
43pub open spec fn index_to_frame(index: int) -> Paddr
44    recommends
45        0 <= index < max_meta_slots(),
46{
47    (index * PAGE_SIZE) as Paddr
48}
49
50/// Converting an in-range metadata-slot index to its frame address and back
51/// preserves the index, and the resulting address is page aligned.
52pub broadcast proof fn lemma_index_to_frame_biinjective(index: int)
53    requires
54        0 <= index < max_meta_slots(),
55    ensures
56        #[trigger] index_to_frame(index) % PAGE_SIZE == 0,
57        frame_to_index(index_to_frame(index)) == index,
58{
59}
60
61/// `frame_to_index` is injective on page-aligned paddrs.
62pub broadcast proof fn lemma_frame_to_index_injective(p1: Paddr, p2: Paddr)
63    requires
64        p1 % PAGE_SIZE == 0,
65        p2 % PAGE_SIZE == 0,
66        p1 != p2,
67    ensures
68        #[trigger] frame_to_index(p1) != #[trigger] frame_to_index(p2),
69{
70}
71
72pub broadcast proof fn lemma_paddr_to_meta_biinjective(paddr: Paddr)
73    requires
74        valid_frame_paddr(paddr),
75    ensures
76        #[trigger] meta_to_frame(frame_to_meta(paddr)) == paddr,
77{
78}
79
80pub broadcast proof fn lemma_meta_to_paddr_biinjective(vaddr: Vaddr)
81    requires
82        FRAME_METADATA_RANGE.start <= vaddr && vaddr < FRAME_METADATA_RANGE.end,
83        vaddr % META_SLOT_SIZE == 0,
84    ensures
85        #[trigger] frame_to_meta(meta_to_frame(vaddr)) == vaddr,
86{
87}
88
89pub broadcast proof fn lemma_meta_to_frame_soundness(meta: Vaddr)
90    requires
91        meta % META_SLOT_SIZE == 0,
92        FRAME_METADATA_RANGE.start <= meta && meta < FRAME_METADATA_RANGE.start + MAX_NR_PAGES
93            * META_SLOT_SIZE,
94    ensures
95        #[trigger] meta_to_frame(meta) % PAGE_SIZE == 0,
96        meta_to_frame(meta) < MAX_PADDR,
97{
98}
99
100pub broadcast proof fn lemma_frame_to_meta_soundness(page: Paddr)
101    requires
102        valid_frame_paddr(page),
103    ensures
104        #[trigger] frame_to_meta(page) % META_SLOT_SIZE == 0,
105        FRAME_METADATA_RANGE.start <= frame_to_meta(page) && frame_to_meta(page)
106            < FRAME_METADATA_RANGE.start + MAX_NR_PAGES * META_SLOT_SIZE,
107{
108}
109
110pub broadcast proof fn lemma_meta_to_frame_alignment(meta: Vaddr)
111    requires
112        meta % META_SLOT_SIZE == 0,
113        FRAME_METADATA_RANGE.start <= meta && meta < FRAME_METADATA_RANGE.start + MAX_NR_PAGES
114            * META_SLOT_SIZE,
115    ensures
116        #[trigger] meta_to_frame(meta) % PAGE_SIZE == 0,
117        meta_to_frame(meta) < MAX_PADDR,
118{
119}
120
121pub broadcast group group_page_meta {
122    lemma_index_to_frame_biinjective,
123    lemma_paddr_to_meta_biinjective,
124    lemma_meta_to_paddr_biinjective,
125    lemma_meta_to_frame_soundness,
126    lemma_frame_to_meta_soundness,
127    lemma_meta_to_frame_alignment,
128}
129
130} // verus!
ostd/specs/mm/frame/mapping.rs

ostd/specs/mm/frame/
mapping.rs
