ostd/specs/arch/
model.rs

1//! Architecture contracts for modeled frames and linear address mappings.
2//!
3//! # Verified Properties
4//!
5//! These erased contracts require each architecture instance to prove that its
6//! modeled physical-address bound is page-aligned and that its linear mapping
7//! has room for those addresses without overflow. The bound limits tracked
8//! memory; it does not describe the processor's physical-address width.
9//! Within each architecture's linear mapping window, the address conversions
10//! preserve bounds and are mutual inverses. Physical-to-virtual conversion also
11//! preserves base-page alignment.
12//! `CurrentArch` selects the instance for this target. Calls to
13//! `PagingConstsTrait::axiom_current_paging_consts_hardcoded` mark proofs that
14//! still depend on the constants used by executable page-table layouts.
15use vstd::prelude::*;
16use vstd_extra::arithmetic::lemma_mod_0_add;
17
18use crate::mm::{Paddr, PagingConstsTrait, Vaddr};
19
20verus! {
21
22/// The architecture contract for modeled physical frames and their linear mapping.
23///
24/// The associated paging constants are still supplied by the existing
25/// `PagingConstsTrait`; this trait supplies the modeled physical-address bound
26/// and the kernel's linear mapping, together with their compatibility proofs.
27pub trait ArchAddressSpaceModel {
28    type C: PagingConstsTrait;
29
30    /// The exclusive upper bound for modeled physical frame addresses.
31    spec fn max_paddr_spec() -> Paddr;
32
33    /// The base of the kernel's physical-to-virtual linear mapping.
34    spec fn linear_mapping_base_vaddr_spec() -> Vaddr;
35
36    /// The first virtual address reserved for vmalloc mappings.
37    spec fn vmalloc_base_vaddr_spec() -> Vaddr;
38
39    /// Proves that the physical range and linear mapping satisfy the model requirements.
40    proof fn lemma_model_requirements()
41        ensures
42            0 < Self::max_paddr_spec(),
43            Self::C::BASE_PAGE_SIZE() <= Self::max_paddr_spec(),
44            Self::max_paddr_spec() % Self::C::BASE_PAGE_SIZE() == 0,
45            Self::linear_mapping_base_vaddr_spec() % Self::C::BASE_PAGE_SIZE() == 0,
46            Self::max_paddr_spec() + Self::linear_mapping_base_vaddr_spec()
47                < Self::vmalloc_base_vaddr_spec(),
48    ;
49}
50
51/// A physical address that can identify a base-page frame for architecture `A`.
52pub open spec fn valid_frame_paddr_for<A: ArchAddressSpaceModel>(pa: Paddr) -> bool {
53    pa % A::C::BASE_PAGE_SIZE() == 0 && pa < A::max_paddr_spec()
54}
55
56/// Convert a physical address through architecture `A`'s linear mapping.
57pub open spec fn paddr_to_vaddr_for<A: ArchAddressSpaceModel>(pa: Paddr) -> Vaddr {
58    (pa + A::linear_mapping_base_vaddr_spec()) as usize
59}
60
61/// Convert a linear-mapped virtual address back to a physical address.
62pub open spec fn vaddr_to_paddr_for<A: ArchAddressSpaceModel>(va: Vaddr) -> Paddr {
63    (va - A::linear_mapping_base_vaddr_spec()) as usize
64}
65
66/// Maps a physical offset into the linear mapping window and back without loss.
67pub proof fn lemma_paddr_to_vaddr_properties_for<A: ArchAddressSpaceModel>(pa: Paddr)
68    requires
69        pa < A::vmalloc_base_vaddr_spec() - A::linear_mapping_base_vaddr_spec(),
70    ensures
71        A::linear_mapping_base_vaddr_spec() <= paddr_to_vaddr_for::<A>(pa)
72            < A::vmalloc_base_vaddr_spec(),
73        vaddr_to_paddr_for::<A>(paddr_to_vaddr_for::<A>(pa)) == pa,
74{
75}
76
77/// Maps a linear-mapped virtual address to a physical offset and back without loss.
78pub proof fn lemma_vaddr_to_paddr_properties_for<A: ArchAddressSpaceModel>(va: Vaddr)
79    requires
80        A::linear_mapping_base_vaddr_spec() <= va < A::vmalloc_base_vaddr_spec(),
81    ensures
82        vaddr_to_paddr_for::<A>(va) < A::vmalloc_base_vaddr_spec()
83            - A::linear_mapping_base_vaddr_spec(),
84        paddr_to_vaddr_for::<A>(vaddr_to_paddr_for::<A>(va)) == va,
85{
86}
87
88/// Preserves base-page alignment when mapping a physical offset into the linear window.
89pub proof fn lemma_paddr_to_vaddr_aligned_for<A: ArchAddressSpaceModel>(pa: Paddr)
90    requires
91        pa < A::vmalloc_base_vaddr_spec() - A::linear_mapping_base_vaddr_spec(),
92        pa % A::C::BASE_PAGE_SIZE() == 0,
93    ensures
94        paddr_to_vaddr_for::<A>(pa) % A::C::BASE_PAGE_SIZE() == 0,
95{
96    A::C::lemma_paging_consts_requirements();
97    A::lemma_model_requirements();
98    lemma_mod_0_add(
99        pa as int,
100        A::linear_mapping_base_vaddr_spec() as int,
101        A::C::BASE_PAGE_SIZE() as int,
102    );
103}
104
105} // verus!
ostd/specs/arch/model.rs

ostd/specs/arch/
model.rs
