ostd/specs/arch/x86/
mod.rs

1use crate::mm::frame::meta::{META_SLOT_SIZE, mapping::meta_to_frame};
2use crate::mm::kspace::FRAME_METADATA_RANGE;
3use crate::mm::kspace::{LINEAR_MAPPING_BASE_VADDR, VMALLOC_BASE_VADDR, paddr_to_vaddr};
4use crate::mm::{Paddr, Vaddr, page_size};
5use crate::specs::mm::frame::mapping::lemma_meta_to_frame_soundness;
6use vstd::prelude::*;
7use vstd_extra::prelude::*;
8
9verus! {
10
11// Asterinas is designed for 64-bit architectures.
12global size_of usize == 8;
13
14global size_of isize == 8;
15
16// The following constants are the same as those defined in `ostd::arch::mm::x86_64`,
17// but we record their actual values for better proof automation.
18/// Page size.
19pub const PAGE_SIZE: usize = 4096;
20
21/// The maximum number of entries in a page table node
22pub const NR_ENTRIES: usize = 512;
23
24/// The maximum level of a page table node.
25pub const NR_LEVELS: usize = 4;
26
27/// Parameterized maximum physical address.
28pub const MAX_PADDR: usize = 0x8000_0000;
29
30pub const MAX_NR_PAGES: u64 = (MAX_PADDR / PAGE_SIZE) as u64;
31
32pub open spec fn has_safe_slot(paddr: Paddr) -> bool {
33    &&& paddr % PAGE_SIZE == 0
34    &&& paddr < MAX_PADDR
35}
36
37} // verus!
38verus! {
39
40pub proof fn lemma_linear_mapping_base_vaddr_properties()
41    ensures
42        LINEAR_MAPPING_BASE_VADDR % PAGE_SIZE == 0,
43        LINEAR_MAPPING_BASE_VADDR < VMALLOC_BASE_VADDR,
44{
45    assert(LINEAR_MAPPING_BASE_VADDR % PAGE_SIZE == 0) by (compute_only);
46    assert(LINEAR_MAPPING_BASE_VADDR < VMALLOC_BASE_VADDR) by (compute_only);
47}
48
49/// There is not an executable version in the source code.
50#[verifier::inline]
51pub open spec fn vaddr_to_paddr(va: Vaddr) -> usize
52    recommends
53        LINEAR_MAPPING_BASE_VADDR <= va < VMALLOC_BASE_VADDR,
54{
55    (va - LINEAR_MAPPING_BASE_VADDR) as usize
56}
57
58pub broadcast proof fn lemma_paddr_to_vaddr_properties(pa: Paddr)
59    requires
60        pa < VMALLOC_BASE_VADDR - LINEAR_MAPPING_BASE_VADDR,
61    ensures
62        LINEAR_MAPPING_BASE_VADDR <= #[trigger] paddr_to_vaddr(pa) < VMALLOC_BASE_VADDR,
63        #[trigger] vaddr_to_paddr(paddr_to_vaddr(pa)) == pa,
64{
65}
66
67pub broadcast proof fn lemma_vaddr_to_paddr_properties(va: Vaddr)
68    requires
69        LINEAR_MAPPING_BASE_VADDR <= va < VMALLOC_BASE_VADDR,
70    ensures
71        #[trigger] vaddr_to_paddr(va) < VMALLOC_BASE_VADDR - LINEAR_MAPPING_BASE_VADDR,
72        #[trigger] paddr_to_vaddr(vaddr_to_paddr(va)) == va,
73{
74}
75
76pub proof fn lemma_max_paddr_range()
77    ensures
78        MAX_PADDR < VMALLOC_BASE_VADDR - LINEAR_MAPPING_BASE_VADDR,
79        MAX_PADDR + LINEAR_MAPPING_BASE_VADDR < usize::MAX,
80{
81    assert(MAX_PADDR < VMALLOC_BASE_VADDR - LINEAR_MAPPING_BASE_VADDR) by (compute_only);
82    assert(MAX_PADDR + LINEAR_MAPPING_BASE_VADDR < usize::MAX) by (compute_only);
83}
84
85pub broadcast proof fn lemma_meta_frame_vaddr_properties(meta: Vaddr)
86    requires
87        meta % META_SLOT_SIZE == 0,
88        FRAME_METADATA_RANGE.start <= meta < FRAME_METADATA_RANGE.start + MAX_NR_PAGES
89            * META_SLOT_SIZE,
90    ensures
91        LINEAR_MAPPING_BASE_VADDR <= #[trigger] paddr_to_vaddr(meta_to_frame(meta))
92            < VMALLOC_BASE_VADDR,
93        #[trigger] paddr_to_vaddr(meta_to_frame(meta)) % PAGE_SIZE == 0,
94{
95    let pa = meta_to_frame(meta);
96    lemma_meta_to_frame_soundness(meta);
97    lemma_max_paddr_range();
98    let va = paddr_to_vaddr(pa);
99    lemma_linear_mapping_base_vaddr_properties();
100    assert(va % PAGE_SIZE == 0) by {
101        lemma_mod_0_add(pa as int, LINEAR_MAPPING_BASE_VADDR as int, PAGE_SIZE as int);
102    };
103}
104
105} // verus!
ostd/specs/arch/x86/mod.rs

ostd/specs/arch/x86/
mod.rs
