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::{
8    arch::{
9        CurrentArch, lemma_max_paddr_range, lemma_paddr_to_vaddr_properties,
10        model::{ArchAddressSpaceModel, lemma_paddr_to_vaddr_aligned_for},
11    },
12    mm::{
13        frame::mapping::lemma_meta_to_frame_soundness,
14        page_table::{
15            leading_bits_spec, nr_page_table_coverage_bits_spec, nr_pte_index_bits_spec,
16            page_table_managed_end_spec, page_table_managed_start_spec, pte_index_bit_offset_spec,
17            vaddr_range_proofs, vaddr_range_spec,
18        },
19    },
20};
21
22use crate::{
23    arch::mm::{NR_ENTRIES, PAGE_SIZE, PagingConsts},
24    mm::{
25        MAX_NR_PAGES, MAX_PADDR, Paddr, PagingConstsTrait, Vaddr,
26        frame::meta::{META_SLOT_SIZE, mapping::meta_to_frame},
27        kspace::{
28            FRAME_METADATA_RANGE, KernelPtConfig, LINEAR_MAPPING_BASE_VADDR, VMALLOC_BASE_VADDR,
29            paddr_to_vaddr,
30        },
31        vm_space::UserPtConfig,
32    },
33};
34
35verus! {
36
37/// The x86 instance of the architecture-wide specification contract.
38pub ghost struct X86Arch;
39
40impl ArchAddressSpaceModel for X86Arch {
41    type C = crate::arch::mm::PagingConsts;
42
43    open spec fn max_paddr_spec() -> Paddr {
44        MAX_PADDR
45    }
46
47    open spec fn linear_mapping_base_vaddr_spec() -> Vaddr {
48        LINEAR_MAPPING_BASE_VADDR
49    }
50
51    open spec fn vmalloc_base_vaddr_spec() -> Vaddr {
52        VMALLOC_BASE_VADDR
53    }
54
55    proof fn lemma_model_requirements() {
56        Self::C::lemma_paging_consts_requirements();
57        assert(Self::linear_mapping_base_vaddr_spec() % Self::C::BASE_PAGE_SIZE() == 0)
58            by (compute_only);
59
60        assert(0 < Self::max_paddr_spec()) by (compute_only);
61        assert(Self::C::BASE_PAGE_SIZE() <= Self::max_paddr_spec()) by (compute_only);
62        assert(Self::max_paddr_spec() % Self::C::BASE_PAGE_SIZE() == 0) by (compute_only);
63        assert(Self::max_paddr_spec() + Self::linear_mapping_base_vaddr_spec()
64            < Self::vmalloc_base_vaddr_spec()) by (compute_only);
65    }
66}
67
68pub broadcast proof fn lemma_meta_frame_vaddr_properties(meta: Vaddr)
69    requires
70        meta % META_SLOT_SIZE == 0,
71        FRAME_METADATA_RANGE.start <= meta < FRAME_METADATA_RANGE.start + MAX_NR_PAGES
72            * META_SLOT_SIZE,
73    ensures
74        LINEAR_MAPPING_BASE_VADDR <= #[trigger] paddr_to_vaddr(meta_to_frame(meta))
75            < VMALLOC_BASE_VADDR,
76        #[trigger] paddr_to_vaddr(meta_to_frame(meta)) % PAGE_SIZE == 0,
77{
78    let pa = meta_to_frame(meta);
79    lemma_meta_to_frame_soundness(meta);
80    lemma_max_paddr_range();
81    lemma_paddr_to_vaddr_properties(pa);
82    lemma_paddr_to_vaddr_aligned_for::<CurrentArch>(pa);
83}
84
85// Here are some architecture-specific const value properties.
86// Any use of this lemma in architecture-independent code should be removed.
87pub(crate) proof fn lemma_arch_specific_consts_properties<C: PagingConstsTrait>()
88    ensures
89        C::BASE_PAGE_SIZE().ilog2() == 12u32,
90        nr_pte_index_bits_spec::<C>() == 9usize,
91        pow2(9) == NR_ENTRIES,
92        pte_index_bit_offset_spec::<C>(4) == 39,
93        0 * pow2(39) == 0,
94        256 * pow2(39) == pow2(47),
95        512 * pow2(39) == pow2(48),
96        pow2(47) - 1 == 0x0000_7FFF_FFFF_FFFF,
97        0xffff_int * 0x1_0000_0000_0000int + pow2(47) == 0xffff_8000_0000_0000int,
98        0xffff_int * 0x1_0000_0000_0000int + pow2(48) - 1 == 0xffff_ffff_ffff_ffffint,
99{
100    C::lemma_paging_consts_properties();
101    C::axiom_current_paging_consts_hardcoded();
102    lemma2_to64();
103    lemma2_to64_rest();
104    lemma_usize_pow2_ilog2(12);
105    lemma_usize_pow2_ilog2(9);
106    lemma_pow2_adds(8, 39);
107}
108
109/// Checks the user address range for x86-64 four-level paging.
110pub(crate) proof fn lemma_vaddr_range_spec_user()
111    ensures
112        leading_bits_spec::<UserPtConfig>() == 0,
113        page_table_managed_start_spec::<UserPtConfig>() == 0,
114        page_table_managed_end_spec::<UserPtConfig>() == 0x0000_8000_0000_0000int,
115        vaddr_range_spec::<UserPtConfig>().start == 0,
116        vaddr_range_spec::<UserPtConfig>().end == 0x0000_7FFF_FFFF_FFFF,
117{
118    lemma_arch_specific_consts_properties::<PagingConsts>();
119    vstd::arithmetic::power2::lemma2_to64();
120    vstd::arithmetic::power2::lemma2_to64_rest();
121}
122
123/// Checks the kernel address range for x86-64 four-level paging.
124pub(crate) proof fn lemma_vaddr_range_spec_kernel()
125    ensures
126        leading_bits_spec::<KernelPtConfig>() == 0xffff,
127        page_table_managed_start_spec::<KernelPtConfig>() == 0xFFFF_8000_0000_0000,
128        page_table_managed_end_spec::<KernelPtConfig>() == 0x1_0000_0000_0000_0000int,
129        vaddr_range_spec::<KernelPtConfig>().start == 0xFFFF_8000_0000_0000,
130        vaddr_range_spec::<KernelPtConfig>().end == 0xFFFF_FFFF_FFFF_FFFF,
131{
132    lemma_arch_specific_consts_properties::<PagingConsts>();
133    vstd::arithmetic::power2::lemma2_to64();
134    vstd::arithmetic::power2::lemma2_to64_rest();
135    vstd::layout::unsigned_int_max_values();
136    assert(nr_page_table_coverage_bits_spec::<PagingConsts>() == 48);
137    vaddr_range_proofs::lemma_leading_bits_properties::<KernelPtConfig>();
138    assert((256 * pow2(39) as int / pow2(47) as int) % 2 == 1);
139}
140
141} // verus!
ostd/specs/arch/x86/mod.rs

ostd/specs/arch/x86/
mod.rs
