ostd/specs/mm/frame/
mapping.rs

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

ostd/specs/mm/frame/
mapping.rs
