Module page_table 

Re-exports

pub use cursor::*;

pub use node::*;

Modules

cursor

mapping_set_lemmas

node

vaddr_range_proofs

Bounded-arithmetic proofs for vaddr_range’s body.

Structs

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

Verification Design

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_grandchildren_none

allocated_empty_node_owner

fresh_node_subtree_satisfies

is_valid_range_spec

lemma_align_down_indices

lemma_aligned_indices_zero

lemma_aligned_vaddr_slack

lemma_inc_slot_indices

lemma_lower_indices_aligned

lemma_next_slot_pte_index

lemma_pte_index_bound

lemma_pte_index_spec_is_div_mod

lemma_same_node_pte_indices_match

lemma_same_node_vaddr_upper_bits_match

lemma_vaddr_of_eq_int

lemma_vaddr_path_aligned

lemma_vaddr_strict_bound

lemma_vaddr_top_index_cell

lemma_vaddr_upper_part_is_align_down

nr_pte_index_bits_spec

page_table_vaddr_bits_spec

pte_index_bit_offset_spec

pte_index_spec

rebase_freshly_allocated_children

rebase_freshly_allocated_children_at

rec_vaddr

sibling_paths_disjoint

top_level_index_width_spec

vaddr

vaddr_at

vaddr_make

vaddr_of

vaddr_range_spec

vaddr_replace_pte_index_spec

vaddr_shift

vaddr_shift_bits

vaddr_upper_bits_spec

vaddr_upper_part_spec

Type Aliases

OwnerSubtree

OwnerSubtree is a TreeNode 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.