Skip to main content

ArchAddressSpaceModel

ostd::specs::arch::model

Trait ArchAddressSpaceModel 

Source 
pub trait ArchAddressSpaceModel {
    type C: PagingConstsTrait;

    // Required methods
    spec fn max_paddr_spec() -> Paddr;
    spec fn linear_mapping_base_vaddr_spec() -> Vaddr;
    spec fn vmalloc_base_vaddr_spec() -> Vaddr;
    proof fn lemma_model_requirements();
}
Expand description

The architecture contract for modeled physical frames and their linear mapping.

The associated paging constants are still supplied by the existing PagingConstsTrait; this trait supplies the modeled physical-address bound and the kernel’s linear mapping, together with their compatibility proofs.

Required Associated Types§

Source

type C: PagingConstsTrait

Required Methods§

Source

spec fn max_paddr_spec() -> Paddr

The exclusive upper bound for modeled physical frame addresses.

Source

spec fn linear_mapping_base_vaddr_spec() -> Vaddr

The base of the kernel’s physical-to-virtual linear mapping.

Source

spec fn vmalloc_base_vaddr_spec() -> Vaddr

The first virtual address reserved for vmalloc mappings.

Source

proof fn lemma_model_requirements()

ensures
0 < Self::max_paddr_spec(),
Self::C::BASE_PAGE_SIZE() <= Self::max_paddr_spec(),
Self::max_paddr_spec() % Self::C::BASE_PAGE_SIZE() == 0,
Self::linear_mapping_base_vaddr_spec() % Self::C::BASE_PAGE_SIZE() == 0,
Self::max_paddr_spec() + Self::linear_mapping_base_vaddr_spec()
    < Self::vmalloc_base_vaddr_spec(),

Proves that the physical range and linear mapping satisfy the model requirements.

Dyn Compatibility§

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementors§

Source§

impl ArchAddressSpaceModel for X86Arch

Source§

type C = PagingConsts