paging: move address, sizes, and utility types to paging crate

[ziqiaozhou]

Create the paging crate and move foundational types from the kernel:

• address.rs (PhysAddr, VirtAddr, Address trait), remove unused VirtPhysPair which was introduced 2 years ago and is no longer used by svsm code.
• sizes.rs (PAGE_SIZE, PAGE_SHIFT, size constants)
• util.rs (align_up, align_down, page_align_up, overlap, bit_mask)
• Associated verus spec/proof files for verification
• paging: move Verus specs and proofs into dedicated dirs
• gate proofs and spec with verus_only

The kernel re-exports these types to maintain API compatibility. Unit tests for utility functions move to paging/src/util.rs.

Move helper functions for #1062. #1062 is based on this PR

[ziqiaozhou]

@joergroedel This PR is the first step for #1062 and #1100. Feel free to drop any comments if you have concerns on this change.

[joergroedel]

A review comment from codex which I am not sure is relevant. Dropping it here for reference:

• [P2] Guard Verus specs with the cfg used by cargo-verus — /home/joro/src/svsm/paging/src/util.rs:12-18. When running the documented cargo verify --features verus flow, cargo-verus passes --cfg verus_keep_ghost (as the existing kernel code and build script expect), not verus_only. With these #[cfg(verus_only)] guards, the moved alignment specs/proofs are not included while the #[verus_spec] annotations still refer to align_up_requires, align_up_ens, etc., so verification builds of the new paging crate will fail once this crate is pulled in by kernel's verus feature.

[ziqiaozhou]

A review comment from codex which I am not sure is relevant. Dropping it here for reference:

• [P2] Guard Verus specs with the cfg used by cargo-verus — /home/joro/src/svsm/paging/src/util.rs:12-18. When running the documented cargo verify --features verus flow, cargo-verus passes --cfg verus_keep_ghost (as the existing kernel code and build script expect), not verus_only. With these #[cfg(verus_only)] guards, the moved alignment specs/proofs are not included while the #[verus_spec] annotations still refer to align_up_requires, align_up_ens, etc., so verification builds of the new paging crate will fail once this crate is pulled in by kernel's verus feature.

This is not related. verus_only and verus_keep_ghost are all applied when we run cargo verus .... Since Feb, 2026, verus_only becomes a publicly documented setting attribute that only makes sense during verification, while verus_keep_ghost is not documented. --features verus is only used to pick dependencies.