ostd/specs/arch/x86/
mod.rs

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

ostd/specs/arch/x86/
mod.rs
