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

ostd/specs/mm/frame/
mapping.rs
