Constants§
- CONST_
META_ SLOT_ SIZE - The constant
META_SLOT_SIZE. Metaslot size.
Functions§
- META_
SLOT_ SIZE - META_
SLOT_ SIZE_ SPEC - frame_
to_ index - frame_
to_ index_ spec - frame_
to_ meta - frame_
to_ meta_ spec - group_
page_ meta - index_
to_ frame - index_
to_ frame_ spec - lemma_
FRAME_ METADATA_ RANGE_ is_ large_ enough - lemma_
FRAME_ METADATA_ RANGE_ is_ page_ aligned - lemma_
frame_ to_ meta_ soundness - lemma_
meta_ to_ frame_ alignment - lemma_
meta_ to_ frame_ soundness - lemma_
meta_ to_ paddr_ biinjective - lemma_
paddr_ to_ meta_ biinjective - max_
meta_ slots - meta_
addr - meta_
to_ frame - meta_
to_ frame_ spec