Module page_table 

Re-exports

pub use cursor::*;

pub use node::*;

Modules

cursor

mapping_set_lemmas

node

Structs

AbstractVaddr

An abstract representation of a virtual address as a sequence of indices, representing the values of the bit-fields that index into each level of the page table.

Mapping

A Mapping maps a virtual address range to a physical address range. Its size, page_size, is fixed and must be one of 4096, 2097152, 1073741824. The va_range and pa_range must be of size page_size and aligned on a page boundary. The property is a bitfield of flags that describe the properties of the mapping.

PageTableOwner

PageTableView

A view of the page table is simply the set of mappings that it contains. Its invariant is a crucial property for memory correctness.

Constants

INC_LEVELS

Functions

allocated_empty_node_owner

axiom_leading_bits_bounded

lemma_vaddr_of_eq_int

lemma_vaddr_strict_bound

page_size_monotonic

rec_vaddr

sibling_paths_disjoint

vaddr

vaddr_at

vaddr_make

vaddr_of

vaddr_shift

vaddr_shift_bits

Type Aliases

OwnerSubtree

OwnerSubtree is a tree Node (from vstd_extra::ghost_tree) containing EntryOwners. It lives in a tree of maximum depth 5. Page table nodes can be at levels 0-3, and their entries are their children at the next level down. This means that level 4, the lowest level, can only contain frame entries as it consists of the entries of level 1 page tables.