ostd/specs/arch/x86_64/
kspace.rs

1use vstd::arithmetic::div_mod::*;
2use vstd::prelude::*;
3
4use super::*;
5use crate::mm::{
6    frame::meta::mapping::{lemma_meta_to_frame_soundness, meta_to_frame},
7    frame::*,
8    kspace::{
9        ADDR_WIDTH_SHIFT, FRAME_METADATA_BASE_VADDR, FRAME_METADATA_CAP_VADDR, KERNEL_BASE_VADDR,
10        KERNEL_END_VADDR, LINEAR_MAPPING_BASE_VADDR, LINEAR_MAPPING_VADDR_RANGE,
11        VMALLOC_BASE_VADDR,
12    },
13    Paddr, PagingConsts, Vaddr,
14};
15use crate::specs::mm::frame::mapping::META_SLOT_SIZE;
16
17use core::ops::Range;
18
19verus! {
20
21/// Kernel virtual address range for storing the page frame metadata.
22pub const FRAME_METADATA_RANGE: Range<Vaddr> = 0xffff_fff0_0000_0000..0xffff_fff0_8000_0000;
23
24#[verifier::inline]
25pub open spec fn paddr_to_vaddr_spec(pa: Paddr) -> usize
26    recommends
27        pa < VMALLOC_BASE_VADDR - LINEAR_MAPPING_BASE_VADDR,
28{
29    (pa + LINEAR_MAPPING_BASE_VADDR) as usize
30}
31
32#[inline(always)]
33#[verifier::when_used_as_spec(paddr_to_vaddr_spec)]
34pub fn paddr_to_vaddr(pa: Paddr) -> (res: usize)
35    requires
36        pa < VMALLOC_BASE_VADDR - LINEAR_MAPPING_BASE_VADDR,
37    ensures
38        res == paddr_to_vaddr_spec(pa),
39{
40    (pa + LINEAR_MAPPING_BASE_VADDR) as usize
41}
42
43pub proof fn lemma_linear_mapping_base_vaddr_properties()
44    ensures
45        LINEAR_MAPPING_BASE_VADDR % PAGE_SIZE == 0,
46        LINEAR_MAPPING_BASE_VADDR < VMALLOC_BASE_VADDR,
47{
48    assert(LINEAR_MAPPING_BASE_VADDR % PAGE_SIZE == 0) by (compute_only);
49    assert(LINEAR_MAPPING_BASE_VADDR < VMALLOC_BASE_VADDR) by (compute_only);
50}
51
52#[verifier::inline]
53pub open spec fn vaddr_to_paddr_spec(va: Vaddr) -> usize
54    recommends
55        LINEAR_MAPPING_BASE_VADDR <= va < VMALLOC_BASE_VADDR,
56{
57    (va - LINEAR_MAPPING_BASE_VADDR) as usize
58}
59
60#[inline(always)]
61#[verifier::when_used_as_spec(vaddr_to_paddr_spec)]
62pub fn vaddr_to_paddr(va: Vaddr) -> (res: usize)
63    requires
64        LINEAR_MAPPING_BASE_VADDR <= va < VMALLOC_BASE_VADDR,
65    ensures
66        res == vaddr_to_paddr(va),
67{
68    (va - LINEAR_MAPPING_BASE_VADDR) as usize
69}
70
71pub broadcast proof fn lemma_paddr_to_vaddr_properties(pa: Paddr)
72    requires
73        pa < VMALLOC_BASE_VADDR - LINEAR_MAPPING_BASE_VADDR,
74    ensures
75        LINEAR_MAPPING_BASE_VADDR <= #[trigger] paddr_to_vaddr(pa) < VMALLOC_BASE_VADDR,
76        #[trigger] vaddr_to_paddr(paddr_to_vaddr(pa)) == pa,
77{
78}
79
80pub broadcast proof fn lemma_vaddr_to_paddr_properties(va: Vaddr)
81    requires
82        LINEAR_MAPPING_BASE_VADDR <= va < VMALLOC_BASE_VADDR,
83    ensures
84        #[trigger] vaddr_to_paddr(va) < VMALLOC_BASE_VADDR - LINEAR_MAPPING_BASE_VADDR,
85        #[trigger] paddr_to_vaddr(vaddr_to_paddr(va)) == va,
86{
87}
88
89pub proof fn lemma_max_paddr_range()
90    ensures
91        MAX_PADDR <= VMALLOC_BASE_VADDR - LINEAR_MAPPING_BASE_VADDR,
92{
93    assert(MAX_PADDR <= VMALLOC_BASE_VADDR - LINEAR_MAPPING_BASE_VADDR) by (compute_only);
94}
95
96pub proof fn lemma_mod_0_add(a: int, b: int, m: int)
97    requires
98        0 < m,
99        a % m == 0,
100        b % m == 0,
101    ensures
102        (a + b) % m == 0,
103{
104    lemma_mod_adds(a, b, m);
105}
106
107pub broadcast proof fn lemma_meta_frame_vaddr_properties(meta: Vaddr)
108    requires
109        meta % META_SLOT_SIZE == 0,
110        FRAME_METADATA_RANGE.start <= meta < FRAME_METADATA_RANGE.start + MAX_NR_PAGES
111            * META_SLOT_SIZE,
112    ensures
113        LINEAR_MAPPING_BASE_VADDR <= #[trigger] paddr_to_vaddr(meta_to_frame(meta))
114            < VMALLOC_BASE_VADDR,
115        #[trigger] paddr_to_vaddr(meta_to_frame(meta)) % PAGE_SIZE == 0,
116{
117    let pa = meta_to_frame(meta);
118    lemma_meta_to_frame_soundness(meta);
119    lemma_max_paddr_range();
120    let va = paddr_to_vaddr(pa);
121    lemma_linear_mapping_base_vaddr_properties();
122    assert(va % PAGE_SIZE == 0) by {
123        lemma_mod_0_add(pa as int, LINEAR_MAPPING_BASE_VADDR as int, PAGE_SIZE as int);
124    };
125}
126
127} // verus!
ostd/specs/arch/x86_64/kspace.rs

ostd/specs/arch/x86_64/
kspace.rs
