Module model 

Architecture contracts for modeled frames and linear address mappings.

Verified Properties

These erased contracts require each architecture instance to prove that its modeled physical-address bound is page-aligned and that its linear mapping has room for those addresses without overflow. The bound limits tracked memory; it does not describe the processor’s physical-address width. Within each architecture’s linear mapping window, the address conversions preserve bounds and are mutual inverses. Physical-to-virtual conversion also preserves base-page alignment. CurrentArch selects the instance for this target. Calls to PagingConstsTrait::axiom_current_paging_consts_hardcoded mark proofs that still depend on the constants used by executable page-table layouts.

Traits

ArchAddressSpaceModel

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

Functions

lemma_paddr_to_vaddr_aligned_for

lemma_paddr_to_vaddr_properties_for

lemma_vaddr_to_paddr_properties_for

paddr_to_vaddr_for

vaddr_to_paddr_for

valid_frame_paddr_for