ostd/specs/arch/x86/
mod.rs

1use vstd::{
2    arithmetic::power2::{lemma_pow2_adds, lemma2_to64, lemma2_to64_rest, pow2},
3    prelude::*,
4};
5use vstd_extra::prelude::*;
6
7use crate::specs::mm::{
8    frame::mapping::lemma_meta_to_frame_soundness,
9    page_table::{nr_pte_index_bits_spec, pte_index_bit_offset_spec},
10};
11
12use crate::mm::{
13    Paddr, PagingConstsTrait, Vaddr,
14    frame::meta::{META_SLOT_SIZE, mapping::meta_to_frame},
15    kspace::{FRAME_METADATA_RANGE, LINEAR_MAPPING_BASE_VADDR, VMALLOC_BASE_VADDR, paddr_to_vaddr},
16    page_size,
17};
18
19verus! {
20
21// Asterinas is designed for 64-bit architectures.
22global size_of usize == 8;
23
24global size_of isize == 8;
25
26// The following constants are the same as those defined in `ostd::arch::mm::x86_64`,
27// but we record their actual values for better proof automation.
28/// Page size.
29pub const PAGE_SIZE: usize = 4096;
30
31/// The maximum number of entries in a page table node
32pub const NR_ENTRIES: usize = 512;
33
34/// The maximum level of a page table node.
35pub const NR_LEVELS: usize = 4;
36
37/// Parameterized maximum physical address.
38pub const MAX_PADDR: usize = 0x8000_0000;
39
40pub const MAX_NR_PAGES: u64 = (MAX_PADDR / PAGE_SIZE) as u64;
41
42pub open spec fn valid_frame_paddr(paddr: Paddr) -> bool {
43    &&& paddr % PAGE_SIZE == 0
44    &&& paddr < MAX_PADDR
45}
46
47} // verus!
48verus! {
49
50pub proof fn lemma_linear_mapping_base_vaddr_properties()
51    ensures
52        LINEAR_MAPPING_BASE_VADDR % PAGE_SIZE == 0,
53        LINEAR_MAPPING_BASE_VADDR < VMALLOC_BASE_VADDR,
54{
55    assert(LINEAR_MAPPING_BASE_VADDR % PAGE_SIZE == 0) by (compute_only);
56    assert(LINEAR_MAPPING_BASE_VADDR < VMALLOC_BASE_VADDR) by (compute_only);
57}
58
59/// There is not an executable version in the source code.
60#[verifier::inline]
61pub open spec fn vaddr_to_paddr(va: Vaddr) -> usize
62    recommends
63        LINEAR_MAPPING_BASE_VADDR <= va < VMALLOC_BASE_VADDR,
64{
65    (va - LINEAR_MAPPING_BASE_VADDR) as usize
66}
67
68pub broadcast proof fn lemma_paddr_to_vaddr_properties(pa: Paddr)
69    requires
70        pa < VMALLOC_BASE_VADDR - LINEAR_MAPPING_BASE_VADDR,
71    ensures
72        LINEAR_MAPPING_BASE_VADDR <= #[trigger] paddr_to_vaddr(pa) < VMALLOC_BASE_VADDR,
73        #[trigger] vaddr_to_paddr(paddr_to_vaddr(pa)) == pa,
74{
75}
76
77pub broadcast proof fn lemma_vaddr_to_paddr_properties(va: Vaddr)
78    requires
79        LINEAR_MAPPING_BASE_VADDR <= va < VMALLOC_BASE_VADDR,
80    ensures
81        #[trigger] vaddr_to_paddr(va) < VMALLOC_BASE_VADDR - LINEAR_MAPPING_BASE_VADDR,
82        #[trigger] paddr_to_vaddr(vaddr_to_paddr(va)) == va,
83{
84}
85
86pub proof fn lemma_max_paddr_range()
87    ensures
88        MAX_PADDR < VMALLOC_BASE_VADDR - LINEAR_MAPPING_BASE_VADDR,
89        MAX_PADDR + LINEAR_MAPPING_BASE_VADDR < usize::MAX,
90{
91    assert(MAX_PADDR < VMALLOC_BASE_VADDR - LINEAR_MAPPING_BASE_VADDR) by (compute_only);
92    assert(MAX_PADDR + LINEAR_MAPPING_BASE_VADDR < usize::MAX) by (compute_only);
93}
94
95pub broadcast proof fn lemma_meta_frame_vaddr_properties(meta: Vaddr)
96    requires
97        meta % META_SLOT_SIZE == 0,
98        FRAME_METADATA_RANGE.start <= meta < FRAME_METADATA_RANGE.start + MAX_NR_PAGES
99            * META_SLOT_SIZE,
100    ensures
101        LINEAR_MAPPING_BASE_VADDR <= #[trigger] paddr_to_vaddr(meta_to_frame(meta))
102            < VMALLOC_BASE_VADDR,
103        #[trigger] paddr_to_vaddr(meta_to_frame(meta)) % PAGE_SIZE == 0,
104{
105    let pa = meta_to_frame(meta);
106    lemma_meta_to_frame_soundness(meta);
107    lemma_max_paddr_range();
108    let va = paddr_to_vaddr(pa);
109    lemma_linear_mapping_base_vaddr_properties();
110    assert(va % PAGE_SIZE == 0) by {
111        lemma_mod_0_add(pa as int, LINEAR_MAPPING_BASE_VADDR as int, PAGE_SIZE as int);
112    };
113}
114
115// Here are some architecture-specific const value properties.
116// Any use of this lemma in architecture-independent code should be removed.
117pub(crate) proof fn lemma_arch_specific_consts_properties<C: PagingConstsTrait>()
118    ensures
119        C::BASE_PAGE_SIZE().ilog2() == 12u32,
120        nr_pte_index_bits_spec::<C>() == 9usize,
121        pow2(9) == NR_ENTRIES,
122        pte_index_bit_offset_spec::<C>(4) == 39,
123        0 * pow2(39) == 0,
124        256 * pow2(39) == pow2(47),
125        512 * pow2(39) == pow2(48),
126        pow2(47) - 1 == 0x0000_7FFF_FFFF_FFFF,
127        0xffff_int * 0x1_0000_0000_0000int + pow2(47) == 0xffff_8000_0000_0000int,
128        0xffff_int * 0x1_0000_0000_0000int + pow2(48) - 1 == 0xffff_ffff_ffff_ffffint,
129{
130    C::lemma_paging_consts_properties();
131    lemma2_to64();
132    lemma2_to64_rest();
133    lemma_usize_pow2_ilog2(12);
134    lemma_usize_pow2_ilog2(9);
135    lemma_usize_pow2_ilog2(12);
136    lemma_usize_pow2_ilog2(9);
137    lemma_pow2_adds(8, 39);
138}
139
140} // verus!
ostd/specs/arch/x86/mod.rs

ostd/specs/arch/x86/
mod.rs
