ostd/specs/arch/
mod.rs

1//! Architecture selection and shared memory specifications.
2//!
3//! # Verified Properties
4//!
5//! [`CurrentArch`] selects the target's implementation of the contracts in [`model`].
6//! The erased [`valid_frame_paddr`] predicate requires base-page alignment and an
7//! address below that implementation's modeled physical-memory bound. Shared
8//! constants are re-exported from the executable architecture and memory modules.
9//! The model's conversion lemmas establish bounds, round trips, and alignment
10//! within the linear mapping window. Page-table proofs that call
11//! [`crate::mm::PagingConstsTrait::axiom_current_paging_consts_hardcoded`] still
12//! trust the current layout; that restriction is not enforced for other configurations.
13use vstd::prelude::*;
14
15use crate::mm::{
16    Paddr, Vaddr,
17    kspace::{LINEAR_MAPPING_BASE_VADDR, VMALLOC_BASE_VADDR, paddr_to_vaddr},
18};
19
20pub mod model;
21pub use model::*;
22
23// Compatibility re-exports for proof modules that still use `specs::arch`.
24// The authoritative values live in the executable memory/architecture modules.
25pub use crate::{
26    arch::mm::{NR_ENTRIES, NR_LEVELS, PAGE_SIZE},
27    mm::{MAX_NR_PAGES, MAX_PADDR},
28};
29
30#[cfg(target_arch = "x86_64")]
31mod x86;
32#[cfg(target_arch = "x86_64")]
33pub use x86::*;
34
35#[cfg(target_arch = "riscv64")]
36mod riscv;
37#[cfg(target_arch = "riscv64")]
38pub use riscv::*;
39
40#[cfg(target_arch = "loongarch64")]
41mod loongarch;
42#[cfg(target_arch = "loongarch64")]
43pub use loongarch::*;
44verus! {
45
46// Asterinas is designed for 64-bit architectures.
47global size_of usize == 8;
48
49global size_of isize == 8;
50
51/// The architecture selected by the current verification target.
52#[cfg(target_arch = "x86_64")]
53pub type CurrentArch = x86::X86Arch;
54
55/// The architecture selected by the current verification target.
56#[cfg(target_arch = "riscv64")]
57pub type CurrentArch = riscv::RiscvArch;
58
59#[cfg(target_arch = "loongarch64")]
60pub type CurrentArch = loongarch::LoongArch;
61
62/// A physical address that can identify a base-page frame on the selected architecture.
63pub open spec fn valid_frame_paddr(paddr: Paddr) -> bool {
64    valid_frame_paddr_for::<CurrentArch>(paddr)
65}
66
67pub proof fn lemma_linear_mapping_base_vaddr_properties()
68    ensures
69        LINEAR_MAPPING_BASE_VADDR % PAGE_SIZE == 0,
70        LINEAR_MAPPING_BASE_VADDR < VMALLOC_BASE_VADDR,
71{
72    CurrentArch::lemma_model_requirements();
73}
74
75/// Converts a virtual address in the linear mapping to a physical address.
76#[verifier::inline]
77pub open spec fn vaddr_to_paddr(va: Vaddr) -> usize
78    recommends
79        LINEAR_MAPPING_BASE_VADDR <= va < VMALLOC_BASE_VADDR,
80{
81    model::vaddr_to_paddr_for::<CurrentArch>(va)
82}
83
84/// Relates the current linear mapping to its architecture model and inverse.
85pub broadcast proof fn lemma_paddr_to_vaddr_properties(pa: Paddr)
86    requires
87        pa < VMALLOC_BASE_VADDR - LINEAR_MAPPING_BASE_VADDR,
88    ensures
89        #[trigger] paddr_to_vaddr(pa) == model::paddr_to_vaddr_for::<CurrentArch>(pa),
90        LINEAR_MAPPING_BASE_VADDR <= #[trigger] paddr_to_vaddr(pa) < VMALLOC_BASE_VADDR,
91        #[trigger] vaddr_to_paddr(paddr_to_vaddr(pa)) == pa,
92{
93    lemma_paddr_to_vaddr_properties_for::<CurrentArch>(pa);
94}
95
96pub broadcast proof fn lemma_vaddr_to_paddr_properties(va: Vaddr)
97    requires
98        LINEAR_MAPPING_BASE_VADDR <= va < VMALLOC_BASE_VADDR,
99    ensures
100        #[trigger] vaddr_to_paddr(va) < VMALLOC_BASE_VADDR - LINEAR_MAPPING_BASE_VADDR,
101        #[trigger] paddr_to_vaddr(vaddr_to_paddr(va)) == va,
102{
103    lemma_vaddr_to_paddr_properties_for::<CurrentArch>(va);
104}
105
106pub proof fn lemma_max_paddr_range()
107    ensures
108        MAX_PADDR < VMALLOC_BASE_VADDR - LINEAR_MAPPING_BASE_VADDR,
109        MAX_PADDR + LINEAR_MAPPING_BASE_VADDR < usize::MAX,
110{
111    CurrentArch::lemma_model_requirements();
112}
113
114} // verus!
ostd/specs/arch/mod.rs

ostd/specs/arch/
mod.rs
