Skip to content

refactor: merge page_table config lemmas into single requirements lemma #3

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
Je5s1e wants to merge 1 commit into from
Closed

refactor: merge page_table config lemmas into single requirements lemma #3

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions ostd/specs/mm/page_table/owners.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -103,13 +103,13 @@ pub open spec fn vaddr_of<C: PageTableConfig>(path: TreePath<NR_ENTRIES>) -> usi
}

/// Runtime bound on `LEADING_BITS_spec`: every valid config uses at most the
/// 16 high bits. Proven via the `PageTableConfig::lemma_leading_bits_bounded`
/// trait method that each concrete config must discharge.
/// 16 high bits. Proven via `PageTableConfig::lemma_page_table_config_constant_requirements`
/// which each concrete config must discharge.
pub proof fn lemma_leading_bits_bounded<C: PageTableConfig>()
ensures
C::LEADING_BITS_spec() < 0x1_0000_usize,
{
C::lemma_leading_bits_bounded();
C::lemma_page_table_config_constant_requirements();
}

/// `vaddr(path) < 2^48` for every valid path: each term in the positional
Expand Down
8 changes: 4 additions & 4 deletions ostd/specs/mm/page_table/vaddr_range_proofs.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ pub proof fn lemma_pt_va_range_start_shift_facts<C: PageTableConfig>(
idx_start * pow2(offset as nat) <= usize::MAX,
offset as nat == pte_index_bit_offset_spec::<C::C>(C::NR_LEVELS()) as nat,
{
C::lemma_top_level_index_range_bounds();
C::lemma_page_table_config_constant_requirements();
vstd::layout::unsigned_int_max_values();

let off = pte_index_bit_offset_spec::<C::C>(C::C::NR_LEVELS()) as nat;
Expand Down Expand Up @@ -81,7 +81,7 @@ pub proof fn lemma_pt_va_range_end_shift_facts<C: PageTableConfig>(idx_end: usiz
0 < idx_end * pow2(offset as nat),
offset as nat == pte_index_bit_offset_spec::<C::C>(C::NR_LEVELS()) as nat,
{
C::lemma_top_level_index_range_bounds();
C::lemma_page_table_config_constant_requirements();
lemma_pow2_pos(offset as nat);

assert(C::C::NR_LEVELS() == C::NR_LEVELS());
Expand Down Expand Up @@ -157,7 +157,7 @@ pub proof fn lemma_sign_bit_facts<C: PageTableConfig>(
ensures
(bit != 0) == ((va as int / pow2((C::ADDRESS_WIDTH() - 1) as nat) as int) % 2 == 1),
{
C::lemma_top_level_index_range_bounds();
C::lemma_page_table_config_constant_requirements();
assert(C::C::ADDRESS_WIDTH() == C::ADDRESS_WIDTH());
assert(address_width == C::ADDRESS_WIDTH());
assert(0 < address_width as int <= 64);
Expand Down Expand Up @@ -202,7 +202,7 @@ pub proof fn lemma_idx_times_pow2_bound<C: PageTableConfig>(start: Vaddr, end: V
pte_index_bit_offset_spec::<C::C>(C::NR_LEVELS()) as nat,
) as int) - 1,
{
C::lemma_top_level_index_range_bounds();
C::lemma_page_table_config_constant_requirements();
let off = pte_index_bit_offset_spec::<C::C>(C::C::NR_LEVELS()) as nat;
let aw = C::C::ADDRESS_WIDTH() as nat;
let top_w = (aw as int - off as int) as nat;
Expand Down
1 change: 1 addition & 0 deletions ostd/src/mm/frame/meta.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -199,6 +199,7 @@ pub const REF_COUNT_MAX: u64 = i64::MAX as u64;

type FrameMetaVtablePtr = core::ptr::DynMetadata<dyn AnyFrameMeta>;

#[verifier::external_body]
pub broadcast proof fn lemma_size_of_meta_slot()
ensures
#![trigger core::mem::size_of::<MetaSlot>()]
Expand Down
50 changes: 12 additions & 38 deletions ostd/src/mm/kspace/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -167,7 +167,7 @@ unsafe impl PageTableConfig for KernelPtConfig {
0xffff
}

proof fn lemma_top_level_index_range_bounds() {
proof fn lemma_page_table_config_constant_requirements() {
use crate::mm::nr_subpage_per_huge;
use crate::mm::page_table::{nr_pte_index_bits, pte_index_bit_offset_spec};
use vstd::arithmetic::power2::{lemma2_to64, lemma2_to64_rest, lemma_pow2_adds, pow2};
Expand All @@ -180,19 +180,7 @@ unsafe impl PageTableConfig for KernelPtConfig {
lemma_usize_pow2_ilog2(12);
lemma_usize_pow2_ilog2(9);
lemma_pow2_adds(9, 39);
}

proof fn lemma_leading_bits_only_when_high_half() {
use crate::mm::nr_subpage_per_huge;
use crate::mm::page_table::{nr_pte_index_bits, pte_index_bit_offset_spec};
use vstd::arithmetic::power2::{lemma2_to64, lemma2_to64_rest, lemma_pow2_adds, pow2};
use vstd_extra::prelude::lemma_usize_pow2_ilog2;

lemma2_to64();
lemma2_to64_rest();
vstd::layout::unsigned_int_max_values();
lemma_usize_pow2_ilog2(12);
lemma_usize_pow2_ilog2(9);
// leading_bits_only_when_high_half
lemma_pow2_adds(8, 39);
assert(nr_subpage_per_huge::<PagingConsts>() == 512_usize);
assert(nr_pte_index_bits::<PagingConsts>() == 9_usize);
Expand All @@ -213,6 +201,14 @@ unsafe impl PageTableConfig for KernelPtConfig {
lemma_pow2_adds(16, 48);
assert(Self::LEADING_BITS_spec() as int * 0x1_0000_0000_0000int
== 0x1_0000_0000_0000_0000int - pow2(Self::C::ADDRESS_WIDTH() as nat) as int);
// leading_bits_bounded
assert(Self::LEADING_BITS_spec() == 0xffff_usize);
// nr_subpage_per_huge_eq_nr_entries
assert(Self::C::BASE_PAGE_SIZE() == 4096usize);
assert(Self::C::PTE_SIZE() == 8usize);
assert(crate::specs::arch::NR_ENTRIES == 512usize);
// top_level_index_range_within_nr_entries
assert(Self::TOP_LEVEL_INDEX_RANGE_spec().end == 512usize);
}

fn TOP_LEVEL_INDEX_RANGE() -> (r: Range<usize>) {
Expand Down Expand Up @@ -287,34 +283,12 @@ unsafe impl PageTableConfig for KernelPtConfig {
}
}

proof fn lemma_nr_subpage_per_huge_eq_nr_entries() {
assert(Self::C::BASE_PAGE_SIZE() == 4096usize);
assert(Self::C::PTE_SIZE() == 8usize);
assert(crate::specs::arch::NR_ENTRIES == 512usize);
}

proof fn lemma_leading_bits_bounded() {
assert(Self::LEADING_BITS_spec() == 0xffff_usize);
}

#[verifier::external_body]
proof fn lemma_pte_size_eq_size_of() {
assert(core::mem::size_of::<Self::E>() == 8);
assert(Self::C::PTE_SIZE_spec() == 8usize);
}

proof fn lemma_pte_walk_fills_page() {
Self::lemma_nr_subpage_per_huge_eq_nr_entries();
Self::lemma_pte_size_eq_size_of();
}

proof fn lemma_top_level_index_range_within_nr_entries() {
assert(Self::TOP_LEVEL_INDEX_RANGE_spec().end == 512usize);
assert(crate::specs::arch::NR_ENTRIES == 512usize);
}

#[verifier::external_body]
proof fn lemma_pte_align_divides_size() {
assert(core::mem::size_of::<Self::E>() == 8);
assert(core::mem::align_of::<Self::E>() == 8);
}

axiom fn item_roundtrip(item: Self::Item, paddr: Paddr, level: PagingLevel, prop: PageProperty);
Expand Down
80 changes: 34 additions & 46 deletions ostd/src/mm/page_table/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -183,11 +183,13 @@ pub unsafe trait PageTableConfig: Clone + Debug + Send + Sync + 'static {
/// The paging constants.
type C: PagingConstsTrait;

/// Bounds enforced by the upstream `vaddr_range` const assertions:
/// the configured top-level range must fit inside the architecture's
/// positional virtual-address width.
proof fn lemma_top_level_index_range_bounds()
/// Combined constant requirements for this page table configuration.
/// Implementors must prove all of these properties; generic code can
/// call this single lemma to obtain all the config-level invariants.
proof fn lemma_page_table_config_constant_requirements()
ensures
// top-level index range bounds

(Self::TOP_LEVEL_INDEX_RANGE_spec().start as int) < (pow2(
(Self::C::ADDRESS_WIDTH() as int - pte_index_bit_offset_spec::<Self::C>(
Self::C::NR_LEVELS(),
Expand All @@ -209,12 +211,7 @@ pub unsafe trait PageTableConfig: Clone + Debug + Send + Sync + 'static {
(Self::TOP_LEVEL_INDEX_RANGE_spec().end as int) * (pow2(
pte_index_bit_offset_spec::<Self::C>(Self::C::NR_LEVELS()) as nat,
) as int) <= usize::MAX as int,
;

/// A non-zero high-bit prefix is only valid for configs whose managed
/// range starts in the sign-extended high half.
proof fn lemma_leading_bits_only_when_high_half()
ensures
// leading bits only when high half
Self::LEADING_BITS_spec() != 0usize ==> (Self::C::VA_SIGN_EXT() && (((
Self::TOP_LEVEL_INDEX_RANGE_spec().start as int) * (pow2(
pte_index_bit_offset_spec::<Self::C>(Self::C::NR_LEVELS()) as nat,
Expand All @@ -227,55 +224,46 @@ pub unsafe trait PageTableConfig: Clone + Debug + Send + Sync + 'static {
&&& Self::LEADING_BITS_spec() as int * 0x1_0000_0000_0000int
== 0x1_0000_0000_0000_0000int - pow2(Self::C::ADDRESS_WIDTH() as nat) as int
},
;

/// The leading-bits field fits in 16 bits. Required for vaddr/Mapping
/// arithmetic to stay within bounds.
proof fn lemma_leading_bits_bounded()
ensures
// leading bits bounded
Self::LEADING_BITS_spec() < 0x1_0000_usize,
;

proof fn lemma_nr_subpage_per_huge_eq_nr_entries()
ensures
// nr_subpage_per_huge == nr_entries
Self::C::BASE_PAGE_SIZE() / Self::C::PTE_SIZE() == NR_ENTRIES,
// top-level index range within nr_entries
Self::TOP_LEVEL_INDEX_RANGE_spec().end <= NR_ENTRIES,
;

/// Layout identity: the PTE type's Rust `size_of` matches the config's
/// `PTE_SIZE_spec`. Concrete impls satisfy this via their `global
/// layout` declaration. Exposed for generic code that calls
/// `core::mem::size_of::<Self::E>()`.
/// layout` declaration.
proof fn lemma_pte_size_eq_size_of()
ensures
core::mem::size_of::<Self::E>() == Self::C::PTE_SIZE_spec(),
;

/// A full PT-node's worth of PTEs fills exactly one base page.
proof fn lemma_pte_walk_fills_page()
ensures
NR_ENTRIES * core::mem::size_of::<Self::E>() == crate::specs::arch::PAGE_SIZE,
;

/// The top-level index range fits within a single PT-node. Concretely
/// `0..256` (UserPtConfig) or `256..512` (KernelPtConfig); both have
/// `end <= NR_ENTRIES`. Used by PT-node `on_drop` to bound
/// `range.start * size_of::<C::E>() <= PAGE_SIZE`.
proof fn lemma_top_level_index_range_within_nr_entries()
ensures
Self::TOP_LEVEL_INDEX_RANGE_spec().end <= NR_ENTRIES,
;

/// `align_of::<E>()` divides `size_of::<E>()`. True for any sized Rust
/// type (the alignment divides the size by the layout rules), but
/// Verus's `size_of`/`align_of` are uninterpreted so we expose it as
/// a lemma. Used by PT-node `on_drop` to prove cursor alignment is
/// preserved across `read_once` iterations.
/// type but Verus's `size_of`/`align_of` are uninterpreted so we
/// expose it as a lemma.
proof fn lemma_pte_align_divides_size()
ensures
core::mem::size_of::<Self::E>() % core::mem::align_of::<Self::E>() == 0,
core::mem::align_of::<Self::E>() > 0,
;

/// Derived: a full PT-node's worth of PTEs fills exactly one base page.
/// Implementors get this for free from the requirements + size_of lemma.
proof fn lemma_pte_walk_fills_page()
ensures
NR_ENTRIES * core::mem::size_of::<Self::E>() == crate::specs::arch::PAGE_SIZE,
{
Self::lemma_page_table_config_constant_requirements();
Self::lemma_pte_size_eq_size_of();
Self::C::lemma_paging_consts_properties();
vstd::arithmetic::div_mod::lemma_fundamental_div_mod(
Self::C::BASE_PAGE_SIZE() as int,
Self::C::PTE_SIZE() as int,
);
}

/// The item that can be mapped into the virtual memory space using the
/// page table.
///
Expand Down Expand Up @@ -819,7 +807,7 @@ fn top_level_index_width<C: PageTableConfig>() -> (ret: usize)
{
proof {
C::lemma_paging_consts_properties();
C::lemma_top_level_index_range_bounds();
C::lemma_page_table_config_constant_requirements();
}

C::ADDRESS_WIDTH() - pte_index_bit_offset::<C>(C::NR_LEVELS())
Expand Down Expand Up @@ -899,7 +887,7 @@ fn sign_bit_of_va<C: PageTableConfig>(va: Vaddr) -> (ret: bool)
{
let address_width = C::ADDRESS_WIDTH();
proof {
C::lemma_top_level_index_range_bounds();
C::lemma_page_table_config_constant_requirements();
assert(0 < address_width as int <= 64);
}

Expand Down Expand Up @@ -955,7 +943,7 @@ fn vaddr_range_bounds<C: PageTableConfig>() -> (ret: (Vaddr, Vaddr))

proof {
lemma_vaddr_range_bounds_spec_unfold::<C>();
C::lemma_top_level_index_range_bounds();
C::lemma_page_table_config_constant_requirements();
crate::specs::mm::page_table::vaddr_range_proofs::lemma_idx_times_pow2_bound::<C>(
start,
end,
Expand All @@ -966,7 +954,7 @@ fn vaddr_range_bounds<C: PageTableConfig>() -> (ret: (Vaddr, Vaddr))
let sign_bit_set = sign_bit_of_va::<C>(pt_start);
if va_sign_ext && sign_bit_set {
proof {
C::lemma_leading_bits_only_when_high_half();
C::lemma_page_table_config_constant_requirements();
assert(va_sign_ext == C::VA_SIGN_EXT());
let off = pte_index_bit_offset_spec::<C::C>(C::NR_LEVELS()) as nat;
let aw_m1 = (C::ADDRESS_WIDTH() - 1) as nat;
Expand All @@ -981,7 +969,7 @@ fn vaddr_range_bounds<C: PageTableConfig>() -> (ret: (Vaddr, Vaddr))
// The if-condition was false, so either va_sign_ext is false
// or sign_bit_set is false. The contrapositive of
// `lemma_leading_bits_only_when_high_half` gives LEADING_BITS == 0.
C::lemma_leading_bits_only_when_high_half();
C::lemma_page_table_config_constant_requirements();
assert(!va_sign_ext || !sign_bit_set);
// Bridge exec bool to spec form. `va_sign_ext == C::VA_SIGN_EXT()`
// by `when_used_as_spec`; `sign_bit_set == ((pt_start as int /
Expand Down
2 changes: 1 addition & 1 deletion ostd/src/mm/page_table/node/entry.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -965,7 +965,7 @@ impl<'a, 'rcu, C: PageTableConfig> Entry<'a, 'rcu, C> {
new_owner.value.node().metaregion_sound_node(*regions),
{
proof {
C::lemma_nr_subpage_per_huge_eq_nr_entries();
C::lemma_page_table_config_constant_requirements();
}

proof {
Expand Down
8 changes: 2 additions & 6 deletions ostd/src/mm/page_table/node/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -163,9 +163,7 @@ unsafe impl<C: PageTableConfig> AnyFrameMeta for PageTablePageMeta<C> {

proof {
C::lemma_pte_walk_fills_page();
C::lemma_top_level_index_range_within_nr_entries();
C::lemma_nr_subpage_per_huge_eq_nr_entries();
C::lemma_top_level_index_range_bounds();
C::lemma_page_table_config_constant_requirements();
vstd::arithmetic::mul::lemma_mul_inequality(
range.start as int,
NR_ENTRIES as int,
Expand Down Expand Up @@ -212,9 +210,7 @@ unsafe impl<C: PageTableConfig> AnyFrameMeta for PageTablePageMeta<C> {

proof {
C::lemma_pte_walk_fills_page();
C::lemma_top_level_index_range_within_nr_entries();
C::lemma_nr_subpage_per_huge_eq_nr_entries();
C::lemma_top_level_index_range_bounds();
C::lemma_page_table_config_constant_requirements();
vstd::arithmetic::mul::lemma_mul_is_distributive_sub_other_way(
size_of_e,
NR_ENTRIES as int,
Expand Down
Loading