Add documentation for vm_space utilities (#335)

* `ghost` into `tracked` for API compatibility

* Support for `Once`

* Update

* vmio: initial layout

* vmio: fix two issues with verus updates

* stage

* Fix `replace` to use parent node owner

* Switch `FramePerm` to `MetaPerm`

* Wrapper around `ManuallyDrop::new()` for cases when it is taking on the role of `into_raw`

* vmio: more APIs

* Fixup remaining proofs after `NeverDrop` change

* Closing various unneessary admits in `cursor.rs`

* Starting virtual pointer work

* More cursor work

* minor updates

* Fix merge

* Fix a verification error

* Remove a file

* `replace_cur_entry`

* Update dv

* Starting on virt_ptr

* Migrating out of aster_common: vm_space

* Migrate from aster_common: io, untyped, pod

* Move specs into main ostd tree

* Move `aster_common` into `ostd`, just in its own directory for now.

* start vmspace stuff

* Virtual pointer

* Specification for memcpy

* Move `page_table/cursor` out of legacy `aster_common` directory.

* Moved `page_table/node` from legacy `aster_common` directory

* Moved `page_table` from legacy `aster_common`

* Moving cursor ownership stuff into `specs`

* Ready to work on `cursor_steps` lemmas

* Remove one lemma that shouldn't hold

* Move owner/view files into specs directory

* Migrate `frame` out of legacy `aster_common`

* Eliminated `extern_const` declarations because we can just use consts now that `aster_common` is gone

* Finished merging the legacy `aster_common` stuff over, some proofs did break in the process

* Some proofs related to consts now need manual intervention; also fixed some consts that got changed somehow.

* Revert "Some proofs related to consts now need manual intervention; also fixed some consts that got changed somehow."

This reverts commit 82141a9.

* Revert "Eliminated `extern_const` declarations because we can just use consts now that `aster_common` is gone"

This reverts commit 5c0fa3d.

Turns out `extern_const` is much easier to prove with even if it's not necessary.

* merge

* merge commits

* minor tweaks

* Move more proof definitions into `specs`

* Admit some of the active proofs to push to public repo

* Reconfigured `PageTableOwner` with new `TreeNodeView` implementation

* CursorOwner changes

* New structure for `move_forward` proof

* Move `move_forward` work

* stage

* vmspace: tried experiment

* Working on `map`, `unmap`, `split...`

* Comment out manual trigger so `do_inc_index` will verify

* Remove empty `aster_common` file

* Remove the last trace of `aster_common`, yay!

* Formatting

* Cursor progress

* Update vm to use `VirtPtr`

* suppress warnings

* fix some proofs

* improve IO owner invariants and overlap specs

* lemma for split

* refine IO invariants and complete missing proofs

* refine some API designs

* prove `dispose_writer`

* more proofs

* Removing admits

* Beginnings of memory model work

* Move virtual pointer stuff to `virt_mem` in `ostd`, because it is really part of the ostd verification rather than a generic library

* sync dv

* fix broken proofs

* verify `dispose_reader`

* Use `NeverDrop` in place of `ManuallyDrop`

* Starting on `Node::alloc`

* refactor the tracked design

* Getting guard_perm out of EntryOwner, phase 1

* Remove `guard_perm` from `EntryOwner` phase 2

* Finished removing `guard_perm` from `NodeOwner` and removing the extraneous `NodeEntryOwner` wrapper.

* Re-verifying things that broke due to moving `guard_perm`

* Reverifiying things that changed due to moving `guard_perm`

* Reducing admits in cursor

* Removing admits

* More admits

* More admits

* Relate `pte` with `EntryOwner` (equivalent to how `Entry` is related

* Structure of `split_if_mapped_huge`

* Change `virt_mem_newer` to use separate frames

* refine some ill-formed specs and proofs

* Add the operations to manipulate the page table and TLB, assuming that the `GlobalMemView` is complete (no floating `MemView` objects)

* update

* `protect_next` uncommented

* Some proofs and trigger updates

* Working on virtual memory example; includes changes to `virt_mem_newer`

* Example with mapping a page

* Split up pre- and post-conditions of `map` for readability

* Tweaking `map` doc example

* Working on `guard_perm` assumptions.

* update

* revert toolchain

* prove `activate_writer`

* Assorted admits

* `CursorView` updated for new specs

* Working on some fiddling conditions about locked nodes

* Fix breaking change in `layout`

* Update dv

* Relating page table nodes to their regions

* Fix the performance issue by moving the branches of `map` out into their own functions.

* Uniqueness of pt guards, stage 1: pt metadata carries correct path

* Added predicate map over trees to deal with some challenging reasoning about all nodes

* Added predicate map over trees

* Working more on inline docs for `vmspace` specs, with hyperlinks to `page_table_cursor_specs.rs`

* Big step toward using Set<Mapping> everywhere

* Clearing admits

* finish vm io

* fix warnings and fmt

* fix triggers

* Admitpocalypse

* Assorted fixes

* `split_if_mapped_huge`

* `query` using view spec

* Fixed issue with the `map` top level proof. Resulted in adding some admits that will need to get fixed.

* Page life cycle criteria for nodes

* Mostly work on `jump` admits.

* Add missing `res`

* Finalize non-duplication theorem, but still need to figure out how best to present it

* First stab at the top-level memory document

* Version numbers in `Cargo.lock`

* Top-level theorems: now with more TLB

* Delete old `virt_mem.rs`

* Simplifying `vm_space` specs

* Documented `linked_list`

* Fixed some lingering admits in `linked_list`

* Working on `vm_space` documentation

* Assorted fixes

* More in-depth tlb modeling, for `unmap`

* Beginning to separate out safety conditions from correctness

* `UniqueFrame` documentation, shifting preconditions to separate safety from correctness

* Working on docs and reorganizing `vm_space`

* Finished `vm_space` documentation (at least for now)

* Make `vm_space_specs` public and not re-exported, for cleaner docs.

* Bullet points for multiple conditions in docs

* Fixed `MetaSlot` vs. `MetaSlotStorage` abstraction issue. `MetaSlotStorage` can be modeled as a cell again!

* `Repr` now supports underlying datatypes with their own permissions, so it's able to realistically apply to `MetaSlot`s now.

* documentation and pretty

* Constructing inner perms from meta perm

* Documentation of `node/mod.rs`

* Using the new ReprPtr more widely

* Rename `NeverDrop` to `ManuallyDrop` and use it in all cases

* Eliminated `dropped_slots`

* Documented `meta` except the "drop" related functions

* Done documenting `meta.rs`

* Simplifying preconitions in `Frame`

* prettier and triggers

* `PCell` migration

* documenting `vm_space`

* documenting the lifecycle of vmspaces

* Working on `Frame<M>` documentation

* Finish `frame/mod.rs` documentation

* Remove `vstd_extra::ManuallyDrop` and some duplicate imports

* Remove duplicat imports

* Fine-tune some documentation

* API update for `VmSpace`

* prettier

* fix a typo

* sync dv

* sync dv

* More documentation for `VmSpace`

* add doc for vm_space utilities

* fix errors

---------

Co-authored-by: SNoAnd <33380099+SNoAnd@users.noreply.github.com>

Author: hiroki-chen