ostd/specs/arch/x86_64/
kspace.rs

1use vstd::arithmetic::div_mod::*;
2use vstd::prelude::*;
3
4use super::*;
5use crate::mm::{
6    Paddr, PagingConsts, Vaddr,
7    frame::meta::mapping::{lemma_meta_to_frame_soundness, meta_to_frame},
8    frame::*,
9    kspace::{
10        ADDR_WIDTH_SHIFT, FRAME_METADATA_BASE_VADDR, FRAME_METADATA_CAP_VADDR, KERNEL_BASE_VADDR,
11        KERNEL_END_VADDR, LINEAR_MAPPING_BASE_VADDR, LINEAR_MAPPING_VADDR_RANGE,
12        VMALLOC_BASE_VADDR,
13    },
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_e000_0000_0000..0xffff_e100_0000_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        MAX_PADDR + LINEAR_MAPPING_BASE_VADDR < usize::MAX,
93{
94    assert(MAX_PADDR < VMALLOC_BASE_VADDR - LINEAR_MAPPING_BASE_VADDR) by (compute_only);
95    assert(MAX_PADDR + LINEAR_MAPPING_BASE_VADDR < usize::MAX) by (compute_only);
96}
97
98pub proof fn lemma_mod_0_add(a: int, b: int, m: int)
99    requires
100        0 < m,
101        a % m == 0,
102        b % m == 0,
103    ensures
104        (a + b) % m == 0,
105{
106    lemma_mod_adds(a, b, m);
107}
108
109pub broadcast proof fn lemma_meta_frame_vaddr_properties(meta: Vaddr)
110    requires
111        meta % META_SLOT_SIZE == 0,
112        FRAME_METADATA_RANGE.start <= meta < FRAME_METADATA_RANGE.start + MAX_NR_PAGES
113            * META_SLOT_SIZE,
114    ensures
115        LINEAR_MAPPING_BASE_VADDR <= #[trigger] paddr_to_vaddr(meta_to_frame(meta))
116            < VMALLOC_BASE_VADDR,
117        #[trigger] paddr_to_vaddr(meta_to_frame(meta)) % PAGE_SIZE == 0,
118{
119    let pa = meta_to_frame(meta);
120    lemma_meta_to_frame_soundness(meta);
121    lemma_max_paddr_range();
122    let va = paddr_to_vaddr(pa);
123    lemma_linear_mapping_base_vaddr_properties();
124    assert(va % PAGE_SIZE == 0) by {
125        lemma_mod_0_add(pa as int, LINEAR_MAPPING_BASE_VADDR as int, PAGE_SIZE as int);
126    };
127}
128
129} // verus!
ostd/specs/arch/x86_64/kspace.rs

ostd/specs/arch/x86_64/
kspace.rs
