Class PageStorageTreeNode

security-monitor/src/core/page_allocator/allocator.rs:337–350

/// Invariant: The whole address space of this node is in addressable memory.
#[rr::invariant("INV_IN_RANGE": "node.(base_address) + (page_size_in_bytes_nat node.(max_node_size)) ≤ MaxInt usize")]
struct PageStorageTreeNode {
    // Page token owned by this node. `None` means that this page token has already been allocated or that it has been divided into smaller
    // pages token that were stored in this node's children.
    #[rr::field("<#>@{{ option }} maybe_page_token")]
    page_token: Option<Page<UnAllocated>>,
    // Specifies what size of the page token can be allocated by exploring the tree starting at this node.
    // Invariant: if page token exist, then the its size is the max allocable size. Otherwise, the max allocable page size is the max
    // allocable page size of children
    #[rr::field("<#>@{{ option }} max_sz")]
    max_allocable_page_size: Option<PageSize>,
    // Invariant: Children store page tokens smaller than the page token stored in the parent node
    #[rr::field("<#> children")]
    children: Vec<Self>,
}

#[rr::context("onceG Σ memory_layout")]
#[rr::context("MachineConfig")]