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::MetaSlot;
9pub use crate::mm::frame::meta::mapping::{
10    frame_to_meta, frame_to_meta_spec, meta_to_frame, meta_to_frame_spec,
11};
12use crate::mm::frame::meta::{meta_slot_size, size_of_meta_slot};
13use crate::mm::{Paddr, Vaddr};
14use crate::specs::arch::kspace::FRAME_METADATA_RANGE;
15use crate::specs::arch::mm::{MAX_NR_PAGES, MAX_PADDR, PAGE_SIZE};
16
17verus! {
18
19/// Metaslot size.
20pub const META_SLOT_SIZE: usize = 64;
21
22pub open spec fn max_meta_slots() -> int {
23    (FRAME_METADATA_RANGE.end - FRAME_METADATA_RANGE.start) / META_SLOT_SIZE as int
24}
25
26pub open spec fn meta_addr(i: usize) -> (res: usize)
27    recommends
28        0 <= i < max_meta_slots() as usize,
29{
30    (FRAME_METADATA_RANGE.start + i * META_SLOT_SIZE) as usize
31}
32
33pub broadcast proof fn lemma_FRAME_METADATA_RANGE_is_page_aligned()
34    ensures
35        #[trigger] FRAME_METADATA_RANGE.start % PAGE_SIZE == 0,
36        FRAME_METADATA_RANGE.end % PAGE_SIZE == 0,
37{
38}
39
40pub broadcast proof fn lemma_FRAME_METADATA_RANGE_is_large_enough()
41    ensures
42        #[trigger] FRAME_METADATA_RANGE.end >= FRAME_METADATA_RANGE.start + MAX_NR_PAGES
43            * META_SLOT_SIZE,
44{
45}
46
47#[verifier::inline]
48pub open spec fn frame_to_index(paddr: Paddr) -> usize
49    recommends
50        paddr % PAGE_SIZE == 0,
51{
52    paddr / PAGE_SIZE
53}
54
55#[verifier::inline]
56pub open spec fn index_to_frame(index: usize) -> Paddr
57    recommends
58        index < max_meta_slots(),
59{
60    (index * PAGE_SIZE) as usize
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        paddr % PAGE_SIZE == 0,
77        paddr < MAX_PADDR,
78    ensures
79        #[trigger] meta_to_frame(frame_to_meta(paddr)) == paddr,
80{
81}
82
83pub broadcast proof fn lemma_meta_to_paddr_biinjective(vaddr: Vaddr)
84    requires
85        FRAME_METADATA_RANGE.start <= vaddr && vaddr < FRAME_METADATA_RANGE.end,
86        vaddr % META_SLOT_SIZE == 0,
87    ensures
88        #[trigger] frame_to_meta(meta_to_frame(vaddr)) == vaddr,
89{
90}
91
92pub broadcast proof fn lemma_meta_to_frame_soundness(meta: Vaddr)
93    requires
94        meta % META_SLOT_SIZE == 0,
95        FRAME_METADATA_RANGE.start <= meta && meta < FRAME_METADATA_RANGE.start + MAX_NR_PAGES
96            * META_SLOT_SIZE,
97    ensures
98        #[trigger] meta_to_frame(meta) % PAGE_SIZE == 0,
99        meta_to_frame(meta) < MAX_PADDR,
100{
101}
102
103pub broadcast proof fn lemma_frame_to_meta_soundness(page: Paddr)
104    requires
105        page % PAGE_SIZE == 0,
106        page < MAX_PADDR,
107    ensures
108        #[trigger] frame_to_meta(page) % META_SLOT_SIZE == 0,
109        FRAME_METADATA_RANGE.start <= frame_to_meta(page) && frame_to_meta(page)
110            < FRAME_METADATA_RANGE.start + MAX_NR_PAGES * META_SLOT_SIZE,
111{
112}
113
114pub broadcast proof fn lemma_meta_to_frame_alignment(meta: Vaddr)
115    requires
116        meta % META_SLOT_SIZE == 0,
117        FRAME_METADATA_RANGE.start <= meta && meta < FRAME_METADATA_RANGE.start + MAX_NR_PAGES
118            * META_SLOT_SIZE,
119    ensures
120        #[trigger] meta_to_frame(meta) % PAGE_SIZE == 0,
121        meta_to_frame(meta) < MAX_PADDR,
122{
123}
124
125pub broadcast group group_page_meta {
126    size_of_meta_slot,
127    lemma_FRAME_METADATA_RANGE_is_page_aligned,
128    lemma_FRAME_METADATA_RANGE_is_large_enough,
129    lemma_paddr_to_meta_biinjective,
130    lemma_meta_to_paddr_biinjective,
131    lemma_meta_to_frame_soundness,
132    lemma_frame_to_meta_soundness,
133    lemma_meta_to_frame_alignment,
134}
135
136} // verus!
ostd/specs/mm/frame/mapping.rs

ostd/specs/mm/frame/
mapping.rs
