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::{
9    META_SLOT_SIZE, MetaSlot,
10    mapping::{frame_to_meta, meta_to_frame},
11};
12use crate::mm::kspace::FRAME_METADATA_RANGE;
13use crate::mm::{Paddr, Vaddr};
14use crate::specs::arch::*;
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
22pub open spec fn meta_addr(i: usize) -> (res: usize)
23    recommends
24        0 <= i < max_meta_slots() as usize,
25{
26    (FRAME_METADATA_RANGE.start + i * META_SLOT_SIZE) as usize
27}
28
29pub broadcast proof fn lemma_FRAME_METADATA_RANGE_is_page_aligned()
30    ensures
31        #[trigger] FRAME_METADATA_RANGE.start % PAGE_SIZE == 0,
32        FRAME_METADATA_RANGE.end % PAGE_SIZE == 0,
33{
34}
35
36pub broadcast proof fn lemma_FRAME_METADATA_RANGE_is_large_enough()
37    ensures
38        #[trigger] FRAME_METADATA_RANGE.end >= FRAME_METADATA_RANGE.start + MAX_NR_PAGES
39            * META_SLOT_SIZE,
40{
41}
42
43#[verifier::inline]
44pub open spec fn frame_to_index(paddr: Paddr) -> usize
45    recommends
46        paddr % PAGE_SIZE == 0,
47{
48    paddr / PAGE_SIZE
49}
50
51#[verifier::inline]
52pub open spec fn index_to_frame(index: usize) -> Paddr
53    recommends
54        index < max_meta_slots(),
55{
56    (index * PAGE_SIZE) as usize
57}
58
59/// `frame_to_index` is injective on page-aligned paddrs.
60pub broadcast proof fn lemma_frame_to_index_injective(p1: Paddr, p2: Paddr)
61    requires
62        p1 % PAGE_SIZE == 0,
63        p2 % PAGE_SIZE == 0,
64        p1 != p2,
65    ensures
66        #[trigger] frame_to_index(p1) != #[trigger] frame_to_index(p2),
67{
68}
69
70pub broadcast proof fn lemma_paddr_to_meta_biinjective(paddr: Paddr)
71    requires
72        paddr % PAGE_SIZE == 0,
73        paddr < MAX_PADDR,
74    ensures
75        #[trigger] meta_to_frame(frame_to_meta(paddr)) == paddr,
76{
77}
78
79pub broadcast proof fn lemma_meta_to_paddr_biinjective(vaddr: Vaddr)
80    requires
81        FRAME_METADATA_RANGE.start <= vaddr && vaddr < FRAME_METADATA_RANGE.end,
82        vaddr % META_SLOT_SIZE == 0,
83    ensures
84        #[trigger] frame_to_meta(meta_to_frame(vaddr)) == vaddr,
85{
86}
87
88pub broadcast proof fn lemma_meta_to_frame_soundness(meta: Vaddr)
89    requires
90        meta % META_SLOT_SIZE == 0,
91        FRAME_METADATA_RANGE.start <= meta && meta < FRAME_METADATA_RANGE.start + MAX_NR_PAGES
92            * META_SLOT_SIZE,
93    ensures
94        #[trigger] meta_to_frame(meta) % PAGE_SIZE == 0,
95        meta_to_frame(meta) < MAX_PADDR,
96{
97}
98
99pub broadcast proof fn lemma_frame_to_meta_soundness(page: Paddr)
100    requires
101        page % PAGE_SIZE == 0,
102        page < MAX_PADDR,
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_FRAME_METADATA_RANGE_is_page_aligned,
123    lemma_FRAME_METADATA_RANGE_is_large_enough,
124    lemma_paddr_to_meta_biinjective,
125    lemma_meta_to_paddr_biinjective,
126    lemma_meta_to_frame_soundness,
127    lemma_frame_to_meta_soundness,
128    lemma_meta_to_frame_alignment,
129}
130
131} // verus!
ostd/specs/mm/frame/mapping.rs

ostd/specs/mm/frame/
mapping.rs
