Module arch 

Architecture selection and shared memory specifications.

Verified Properties

CurrentArch selects the target’s implementation of the contracts in model. The erased valid_frame_paddr predicate requires base-page alignment and an address below that implementation’s modeled physical-memory bound. Shared constants are re-exported from the executable architecture and memory modules. The model’s conversion lemmas establish bounds, round trips, and alignment within the linear mapping window. Page-table proofs that call crate::mm::PagingConstsTrait::axiom_current_paging_consts_hardcoded still trust the current layout; that restriction is not enforced for other configurations.

Re-exports

pub use crate::mm::MAX_NR_PAGES;

pub use crate::mm::MAX_PADDR;

pub use model::*;

Modules

model

Architecture contracts for modeled frames and linear address mappings.

Structs

X86Arch

The x86 instance of the architecture-wide specification contract.

Constants

NR_ENTRIES

Number of entries in an x86-64 page-table node.

NR_LEVELS

Number of translation levels used by the current x86-64 configuration.

PAGE_SIZE

Size of a base page on x86-64.

Functions

lemma_linear_mapping_base_vaddr_properties

lemma_max_paddr_range

lemma_meta_frame_vaddr_properties

lemma_paddr_to_vaddr_properties

lemma_vaddr_to_paddr_properties

vaddr_to_paddr

valid_frame_paddr

Type Aliases

CurrentArch

The architecture selected by the current verification target.