ostd/specs/arch/x86_64/
kspace.rs

1use vstd::arithmetic::div_mod::*;
2use vstd::prelude::*;
3use vstd_extra::extern_const::*;
4
5use super::*;
6use crate::mm::{
7    frame::meta::mapping::{lemma_meta_to_frame_soundness, meta_to_frame},
8    frame::*,
9    Paddr, PagingConsts, Vaddr,
10};
11use crate::specs::mm::frame::mapping::META_SLOT_SIZE;
12
13use core::ops::Range;
14
15extern_const!(
16/// The shortest supported address width is 39 bits. And the literal
17/// values are written for 48 bits address width. Adjust the values
18/// by arithmetic left shift.
19pub ADDR_WIDTH_SHIFT [ADDR_WIDTH_SHIFT_SPEC, CONST_ADDR_WIDTH_SHIFT]:
20    isize = /* PagingConsts::ADDRESS_WIDTH() */ 48 - 48
21);
22
23extern_const!(
24/// Start of the kernel address space.
25/// This is the _lowest_ address of the x86-64's _high_ canonical addresses.
26pub KERNEL_BASE_VADDR [KERNEL_BASE_VADDR_SPEC, CONST_KERNEL_BASE_VADDR]:
27    Vaddr = 0xffff_8000_0000_0000_usize << CONST_ADDR_WIDTH_SHIFT
28);
29
30extern_const!(
31/// End of the kernel address space (non inclusive).
32pub KERNEL_END_VADDR [KERNEL_END_VADDR_SPEC, CONST_KERNEL_END_VADDR]:
33    Vaddr = 0xffff_ffff_ffff_0000_usize << CONST_ADDR_WIDTH_SHIFT
34);
35
36extern_const!(
37/// Kernel virtual address range for storing the page frame metadata.
38pub FRAME_METADATA_RANGE
39    [FRAME_METADATA_RANGE_SPEC, CONST_FRAME_METADATA_RANGE]: Range<Vaddr>
40    = 0xffff_fff0_0000_0000..0xffff_fff0_8000_0000
41);
42
43extern_const!(
44pub FRAME_METADATA_CAP_VADDR [FRAME_METADATA_CAP_VADDR_SPEC, CONST_FRAME_METADATA_CAP_VADDR]:
45    Vaddr = 0xffff_fff0_8000_0000_usize << CONST_ADDR_WIDTH_SHIFT
46);
47
48extern_const!(
49pub FRAME_METADATA_BASE_VADDR [FRAME_METADATA_BASE_VADDR_SPEC, CONST_FRAME_METADATA_BASE_VADDR]:
50    Vaddr = 0xffff_fff0_0000_0000_usize << CONST_ADDR_WIDTH_SHIFT
51);
52
53extern_const!(
54pub LINEAR_MAPPING_BASE_VADDR [LINEAR_MAPPING_BASE_VADDR_SPEC, CONST_LINEAR_MAPPING_BASE_VADDR]:
55    Vaddr = 0xffff_8000_0000_0000_usize << CONST_ADDR_WIDTH_SHIFT
56);
57
58extern_const!(
59pub VMALLOC_BASE_VADDR [VMALLOC_BASE_VADDR_SPEC, CONST_VMALLOC_BASE_VADDR]:
60    Vaddr = 0xffff_fd00_0000_0000_usize << CONST_ADDR_WIDTH_SHIFT
61);
62
63extern_const!(
64pub LINEAR_MAPPING_VADDR_RANGE [LINEAR_MAPPING_VADDR_RANGE_SPEC, CONST_LINEAR_MAPPING_VADDR_RANGE]:
65    Range<Vaddr> = CONST_LINEAR_MAPPING_BASE_VADDR..CONST_VMALLOC_BASE_VADDR
66);
67
68verus! {
69
70#[verifier::inline]
71pub open spec fn paddr_to_vaddr_spec(pa: Paddr) -> usize
72    recommends
73        pa < VMALLOC_BASE_VADDR() - LINEAR_MAPPING_BASE_VADDR(),
74{
75    (pa + LINEAR_MAPPING_BASE_VADDR()) as usize
76}
77
78#[inline(always)]
79#[verifier::when_used_as_spec(paddr_to_vaddr_spec)]
80pub fn paddr_to_vaddr(pa: Paddr) -> (res: usize)
81    requires
82        pa < VMALLOC_BASE_VADDR() - LINEAR_MAPPING_BASE_VADDR(),
83    ensures
84        res == paddr_to_vaddr_spec(pa),
85{
86    (pa + LINEAR_MAPPING_BASE_VADDR()) as usize
87}
88
89pub proof fn lemma_linear_mapping_base_vaddr_properties()
90    ensures
91        LINEAR_MAPPING_BASE_VADDR() % PAGE_SIZE() == 0,
92        LINEAR_MAPPING_BASE_VADDR() < VMALLOC_BASE_VADDR(),
93{
94    assert(LINEAR_MAPPING_BASE_VADDR() == 0xffff_8000_0000_0000) by (compute_only);
95    assert(VMALLOC_BASE_VADDR() == 0xffff_fd00_0000_0000) by (compute_only);
96}
97
98#[verifier::inline]
99pub open spec fn vaddr_to_paddr_spec(va: Vaddr) -> usize
100    recommends
101        LINEAR_MAPPING_BASE_VADDR() <= va < VMALLOC_BASE_VADDR(),
102{
103    (va - LINEAR_MAPPING_BASE_VADDR()) as usize
104}
105
106#[inline(always)]
107#[verifier::when_used_as_spec(vaddr_to_paddr_spec)]
108pub fn vaddr_to_paddr(va: Vaddr) -> (res: usize)
109    requires
110        LINEAR_MAPPING_BASE_VADDR() <= va < VMALLOC_BASE_VADDR(),
111    ensures
112        res == vaddr_to_paddr(va),
113{
114    (va - LINEAR_MAPPING_BASE_VADDR()) as usize
115}
116
117pub broadcast proof fn lemma_paddr_to_vaddr_properties(pa: Paddr)
118    requires
119        pa < VMALLOC_BASE_VADDR() - LINEAR_MAPPING_BASE_VADDR(),
120    ensures
121        LINEAR_MAPPING_BASE_VADDR() <= #[trigger] paddr_to_vaddr(pa) < VMALLOC_BASE_VADDR(),
122        #[trigger] vaddr_to_paddr(paddr_to_vaddr(pa)) == pa,
123{
124}
125
126pub broadcast proof fn lemma_vaddr_to_paddr_properties(va: Vaddr)
127    requires
128        LINEAR_MAPPING_BASE_VADDR() <= va < VMALLOC_BASE_VADDR(),
129    ensures
130        #[trigger] vaddr_to_paddr(va) < VMALLOC_BASE_VADDR() - LINEAR_MAPPING_BASE_VADDR(),
131        #[trigger] paddr_to_vaddr(vaddr_to_paddr(va)) == va,
132{
133}
134
135pub proof fn lemma_max_paddr_range()
136    ensures
137        MAX_PADDR() <= VMALLOC_BASE_VADDR() - LINEAR_MAPPING_BASE_VADDR(),
138{
139    assert(VMALLOC_BASE_VADDR() == 0xffff_fd00_0000_0000) by (compute_only);
140    assert(LINEAR_MAPPING_BASE_VADDR() == 0xffff_8000_0000_0000) by (compute_only);
141    assert(VMALLOC_BASE_VADDR() - LINEAR_MAPPING_BASE_VADDR() == 0x7d00_0000_0000);
142    assert(MAX_PADDR() == 0x8000_0000);
143}
144
145pub proof fn lemma_mod_0_add(a: int, b: int, m: int)
146    requires
147        0 < m,
148        a % m == 0,
149        b % m == 0,
150    ensures
151        (a + b) % m == 0,
152{
153    lemma_mod_adds(a, b, m);
154}
155
156pub broadcast proof fn lemma_meta_frame_vaddr_properties(meta: Vaddr)
157    requires
158        meta % META_SLOT_SIZE() == 0,
159        FRAME_METADATA_RANGE().start <= meta < FRAME_METADATA_RANGE().start + MAX_NR_PAGES()
160            * META_SLOT_SIZE(),
161    ensures
162        LINEAR_MAPPING_BASE_VADDR() <= #[trigger] paddr_to_vaddr(meta_to_frame(meta))
163            < VMALLOC_BASE_VADDR(),
164        #[trigger] paddr_to_vaddr(meta_to_frame(meta)) % PAGE_SIZE() == 0,
165{
166    let pa = meta_to_frame(meta);
167    lemma_meta_to_frame_soundness(meta);
168    assert(pa < MAX_PADDR());
169    assert(pa % PAGE_SIZE() == 0);
170    lemma_max_paddr_range();
171    assert(pa < VMALLOC_BASE_VADDR() - LINEAR_MAPPING_BASE_VADDR());
172    let va = paddr_to_vaddr(pa);
173    lemma_linear_mapping_base_vaddr_properties();
174    assert(LINEAR_MAPPING_BASE_VADDR() % PAGE_SIZE() == 0);
175    assert(va % PAGE_SIZE() == 0) by {
176        lemma_mod_0_add(pa as int, LINEAR_MAPPING_BASE_VADDR() as int, PAGE_SIZE() as int);
177    };
178}
179
180} // verus!
ostd/specs/arch/x86_64/kspace.rs

ostd/specs/arch/x86_64/
kspace.rs
