From 60c048f3cc64d956d9a09aabe01b84f9b0d01d9c Mon Sep 17 00:00:00 2001 From: Je5s1e Date: Thu, 6 Aug 2026 22:58:12 +0800 Subject: [PATCH] Verify RISC-V MM with generic paging abstractions --- ostd/specs/arch/model.rs | 179 +++ ostd/specs/arch/riscv/mod.rs | 431 +++++++ ostd/specs/arch/x86/mod.rs | 84 +- ostd/specs/mm/page_table/cursor/owners.rs | 3 +- ostd/specs/mod.rs | 2 + ostd/src/arch/riscv/mm/mod.rs | 1326 +++++++++++++++++++-- ostd/src/arch/x86/mm/mod.rs | 12 +- ostd/src/mm/kspace/mod.rs | 3 +- ostd/src/mm/mod.rs | 70 +- ostd/src/mm/page_table/cursor/mod.rs | 6 +- ostd/src/mm/page_table/mod.rs | 22 +- ostd/src/mm/page_table/node/mod.rs | 25 +- ostd/src/mm/vm_space.rs | 3 +- 13 files changed, 2032 insertions(+), 134 deletions(-) create mode 100644 ostd/specs/arch/model.rs create mode 100644 ostd/specs/arch/riscv/mod.rs diff --git a/ostd/specs/arch/model.rs b/ostd/specs/arch/model.rs new file mode 100644 index 000000000..b6e22e4a9 --- /dev/null +++ b/ostd/specs/arch/model.rs @@ -0,0 +1,179 @@ +use crate::mm::{Paddr, PagingConstsTrait, Vaddr}; +use vstd::arithmetic::power2::*; +use vstd::prelude::*; +use vstd_extra::prelude::lemma_pow2_is_pow2_to64; + +verus! { + +/// The paging-related part of an architecture contract. +/// +/// The associated paging constants are still supplied by the existing +/// `PagingConstsTrait`; this trait only adds the architecture-wide physical +/// address bound and the proof that the two contracts are compatible. +pub trait ArchPagingModel { + type C: PagingConstsTrait; + + /// The exclusive upper bound for physical frame addresses. + spec fn max_paddr_spec() -> Paddr; + + proof fn lemma_paging_model_requirements() + ensures + 0 < Self::max_paddr_spec(), + Self::C::BASE_PAGE_SIZE() <= Self::max_paddr_spec(), + Self::max_paddr_spec() % Self::C::BASE_PAGE_SIZE() == 0, + ; +} + +/// A physical address that can identify a base-page frame for architecture `A`. +pub open spec fn valid_frame_paddr_for(pa: Paddr) -> bool { + pa % A::C::BASE_PAGE_SIZE() == 0 && pa < A::max_paddr_spec() +} + +/// The address-space part of an architecture contract. +pub trait ArchAddressSpaceModel: ArchPagingModel { + /// The base of the kernel's physical-to-virtual linear mapping. + spec fn linear_mapping_base_vaddr_spec() -> Vaddr; + + /// The first virtual address reserved for vmalloc mappings. + spec fn vmalloc_base_vaddr_spec() -> Vaddr; + + proof fn lemma_address_space_model_requirements() + ensures + Self::linear_mapping_base_vaddr_spec() % Self::C::BASE_PAGE_SIZE() == 0, + Self::linear_mapping_base_vaddr_spec() < Self::vmalloc_base_vaddr_spec(), + Self::max_paddr_spec() < Self::vmalloc_base_vaddr_spec() + - Self::linear_mapping_base_vaddr_spec(), + Self::max_paddr_spec() + Self::linear_mapping_base_vaddr_spec() < usize::MAX, + ; +} + +/// Convert a physical address through architecture `A`'s linear mapping. +pub open spec fn paddr_to_vaddr_for(pa: Paddr) -> Vaddr { + (pa + A::linear_mapping_base_vaddr_spec()) as usize +} + +/// Convert a linear-mapped virtual address back to a physical address. +pub open spec fn vaddr_to_paddr_for(va: Vaddr) -> Paddr { + (va - A::linear_mapping_base_vaddr_spec()) as usize +} + +/// The top-level contract used by architecture-independent specifications. +pub trait ArchTrait: ArchAddressSpaceModel { + +} + +/// A proof-only Sv39 paging configuration. +/// +/// This configuration exercises the generic page-table arithmetic with three +/// translation levels. It is deliberately independent from the RISC-V runtime +/// target, which currently activates Sv48. +#[verifier::allow(autoderive_clone_without_spec)] +#[derive(Clone, Debug, Default)] +pub struct Sv39PagingConsts; + +impl PagingConstsTrait for Sv39PagingConsts { + #[verifier::inline] + open spec fn BASE_PAGE_SIZE_spec() -> usize { + 4096 + } + + fn BASE_PAGE_SIZE() -> usize { + 4096 + } + + #[verifier::inline] + open spec fn NR_LEVELS_spec() -> crate::mm::PagingLevel { + 3 + } + + fn NR_LEVELS() -> crate::mm::PagingLevel { + 3 + } + + #[verifier::inline] + open spec fn HIGHEST_TRANSLATION_LEVEL_spec() -> crate::mm::PagingLevel { + 3 + } + + fn HIGHEST_TRANSLATION_LEVEL() -> crate::mm::PagingLevel { + 3 + } + + #[verifier::inline] + open spec fn PTE_SIZE_spec() -> usize { + 8 + } + + fn PTE_SIZE() -> usize { + 8 + } + + #[verifier::inline] + open spec fn ADDRESS_WIDTH_spec() -> usize { + 39 + } + + fn ADDRESS_WIDTH() -> usize { + 39 + } + + #[verifier::inline] + open spec fn VA_SIGN_EXT_spec() -> bool { + true + } + + fn VA_SIGN_EXT() -> bool { + true + } + + proof fn lemma_paging_consts_requirements() { + lemma_pow2_is_pow2_to64(); + lemma2_to64(); + lemma2_to64_rest(); + assert(usize::BITS == 64) by (compute); + vstd::layout::unsigned_int_max_values(); + vstd_extra::external::ilog2::lemma_usize_pow2_ilog2(9); + vstd_extra::external::ilog2::lemma_usize_pow2_ilog2(12); + lemma_pow2_adds(9, 30); + } +} + +/// Regression facts for the generic page-size formula. +pub proof fn lemma_sv39_page_size_formula() + ensures + crate::mm::page_size_for_spec::(1) == 4096, + crate::mm::page_size_for_spec::(2) == 2_097_152, + crate::mm::page_size_for_spec::(3) == 1_073_741_824, + crate::mm::page_size_for_spec::(4) == 549_755_813_888, +{ + Sv39PagingConsts::lemma_paging_consts_properties(); + vstd_extra::external::ilog2::lemma_usize_ilog2_to32(); + lemma2_to64(); + lemma2_to64_rest(); + assert(Sv39PagingConsts::BASE_PAGE_SIZE_spec() == 4096usize) by (compute_only); + assert(Sv39PagingConsts::PTE_SIZE_spec() == 8usize) by (compute_only); + assert(crate::mm::nr_subpage_per_huge_spec::() + == Sv39PagingConsts::BASE_PAGE_SIZE_spec() / Sv39PagingConsts::PTE_SIZE_spec()); + assert(crate::mm::nr_subpage_per_huge_spec::() == 512usize) by { + assert(Sv39PagingConsts::BASE_PAGE_SIZE_spec() / Sv39PagingConsts::PTE_SIZE_spec() + == 512usize); + } + assert(crate::mm::nr_subpage_per_huge_spec::().ilog2() == 9u32) by { + assert(pow2(9nat) as usize == 512usize); + vstd_extra::external::ilog2::lemma_usize_pow2_ilog2(9); + } + vstd::bits::lemma_usize_pow2_no_overflow(18); + vstd::bits::lemma_usize_pow2_no_overflow(27); + assert(pow2(18nat) == 262144nat); + assert(pow2(27nat) == 134217728nat); + assert((9u32 * (3u8 - 1u8)) as nat == 18nat) by (compute_only); + assert((9u32 * (4u8 - 1u8)) as nat == 27nat) by (compute_only); + assert(crate::mm::page_size_for_spec::(1) == 4096usize); + assert(crate::mm::page_size_for_spec::(2) == 4096usize * 512usize); + assert(crate::mm::page_size_for_spec::(3) == 4096usize * 512usize * 512usize); + assert(crate::mm::page_size_for_spec::(4) == 4096usize * 512usize * 512usize + * 512usize); + vstd::bits::lemma_usize_pow2_no_overflow(39); +} + +} // verus! diff --git a/ostd/specs/arch/riscv/mod.rs b/ostd/specs/arch/riscv/mod.rs new file mode 100644 index 000000000..3eb003fd9 --- /dev/null +++ b/ostd/specs/arch/riscv/mod.rs @@ -0,0 +1,431 @@ +use crate::mm::{ + Paddr, PagingConstsTrait, PagingLevel, + page_prop::{CachePolicy, PageFlags, PageProperty, PrivilegedPageFlags}, +}; +use vstd::arithmetic::power2::*; +use vstd::prelude::*; +use vstd_extra::{ownership::Inv, prelude::lemma_pow2_is_pow2_to64}; + +use crate::specs::arch::model::ArchPagingModel; + +#[path = "../../../src/arch/riscv/mm/mod.rs"] +pub mod runtime_mm; + +verus! { + +/// Exclusive physical-address bound represented by an Sv48 PTE's 44-bit PPN. +pub const RISCV_SV48_MAX_PADDR: usize = 0x0100_0000_0000_0000; + +/// Proof-side paging constants for the Sv48 mode selected by the RISC-V runtime. +#[verifier::allow(autoderive_clone_without_spec)] +#[derive(Clone, Debug, Default)] +pub struct RiscvSv48PagingConsts; + +impl PagingConstsTrait for RiscvSv48PagingConsts { + #[verifier::inline] + open spec fn BASE_PAGE_SIZE_spec() -> usize { + 4096 + } + + fn BASE_PAGE_SIZE() -> usize { + 4096 + } + + #[verifier::inline] + open spec fn NR_LEVELS_spec() -> PagingLevel { + 4 + } + + fn NR_LEVELS() -> PagingLevel { + 4 + } + + #[verifier::inline] + open spec fn HIGHEST_TRANSLATION_LEVEL_spec() -> PagingLevel { + 4 + } + + fn HIGHEST_TRANSLATION_LEVEL() -> PagingLevel { + 4 + } + + #[verifier::inline] + open spec fn PTE_SIZE_spec() -> usize { + 8 + } + + fn PTE_SIZE() -> usize { + 8 + } + + #[verifier::inline] + open spec fn ADDRESS_WIDTH_spec() -> usize { + 48 + } + + fn ADDRESS_WIDTH() -> usize { + 48 + } + + #[verifier::inline] + open spec fn VA_SIGN_EXT_spec() -> bool { + true + } + + fn VA_SIGN_EXT() -> bool { + true + } + + proof fn lemma_paging_consts_requirements() { + lemma_pow2_is_pow2_to64(); + lemma2_to64(); + lemma2_to64_rest(); + assert(usize::BITS == 64) by (compute); + vstd::layout::unsigned_int_max_values(); + vstd_extra::external::ilog2::lemma_usize_pow2_ilog2(9); + vstd_extra::external::ilog2::lemma_usize_pow2_ilog2(12); + lemma_pow2_adds(9, 39); + } +} + +/// Paging-only RISC-V architecture instance. Address-space layout is modeled later. +pub struct RiscvPagingModel; + +impl ArchPagingModel for RiscvPagingModel { + type C = RiscvSv48PagingConsts; + + open spec fn max_paddr_spec() -> Paddr { + RISCV_SV48_MAX_PADDR + } + + proof fn lemma_paging_model_requirements() { + RiscvSv48PagingConsts::lemma_paging_consts_requirements(); + assert(0 < RISCV_SV48_MAX_PADDR) by (compute_only); + assert(4096 <= RISCV_SV48_MAX_PADDR) by (compute_only); + assert(RISCV_SV48_MAX_PADDR % 4096 == 0) by (compute_only); + } +} + +/// A proof model of the architectural bits in a RISC-V Sv48 page-table entry. +#[derive(Clone, Copy, PartialEq, Eq)] +pub struct RiscvPteModel { + pub raw: usize, +} + +impl RiscvPteModel { + pub const VALID: usize = 1 << 0; + + pub const READABLE: usize = 1 << 1; + + pub const WRITABLE: usize = 1 << 2; + + pub const EXECUTABLE: usize = 1 << 3; + + pub const USER: usize = 1 << 4; + + pub const GLOBAL: usize = 1 << 5; + + pub const ACCESSED: usize = 1 << 6; + + pub const DIRTY: usize = 1 << 7; + + pub const RSW1: usize = 1 << 8; + + pub const RSW2: usize = 1 << 9; + + pub const PBMT_IO: usize = 1 << 62; + + pub const PHYS_ADDR_MASK: usize = 0x003F_FFFF_FFFF_FC00; + + pub open spec fn paddr_bits(paddr: Paddr) -> usize { + (paddr >> 12) << 10 + } + + pub open spec fn paddr_from_raw_spec(raw: usize) -> Paddr { + ((raw & Self::PHYS_ADDR_MASK) >> 10) << 12 + } + + pub open spec fn paddr_spec(self) -> Paddr { + Self::paddr_from_raw_spec(self.raw) + } + + pub open spec fn is_present_spec(self) -> bool { + self.raw & Self::VALID != 0 + } + + pub open spec fn is_last_spec(self, _level: PagingLevel) -> bool { + self.raw & (Self::READABLE | Self::WRITABLE | Self::EXECUTABLE) != 0 + } + + pub open spec fn encode_page_flags_spec(prop: PageProperty) -> usize { + (if prop.flags.bits() & 0x01u8 != 0 { + Self::READABLE + } else { + 0 + }) | (if prop.flags.bits() & 0x02u8 != 0 { + Self::WRITABLE + } else { + 0 + }) | (if prop.flags.bits() & 0x04u8 != 0 { + Self::EXECUTABLE + } else { + 0 + }) | (if prop.flags.bits() & 0x08u8 != 0 { + Self::ACCESSED + } else { + 0 + }) | (if prop.flags.bits() & 0x10u8 != 0 { + Self::DIRTY + } else { + 0 + }) | (if prop.flags.bits() & 0x40u8 != 0 { + Self::RSW1 + } else { + 0 + }) | (if prop.flags.bits() & 0x80u8 != 0 { + Self::RSW2 + } else { + 0 + }) + } + + pub open spec fn encode_priv_flags_spec(prop: PageProperty) -> usize { + (if prop.priv_flags.bits() & 0x01u8 != 0 { + Self::USER + } else { + 0 + }) | (if prop.priv_flags.bits() & 0x02u8 != 0 { + Self::GLOBAL + } else { + 0 + }) + } + + pub open spec fn encode_cache_spec(prop: PageProperty) -> usize { + if prop.cache is Uncacheable { + Self::PBMT_IO + } else { + 0 + } + } + + pub open spec fn property_bits_from_parts_spec( + flags: u8, + priv_flags: u8, + cache: CachePolicy, + ) -> usize { + Self::VALID | (if flags & 0x01u8 != 0 { + Self::READABLE + } else { + 0 + }) | (if flags & 0x02u8 != 0 { + Self::WRITABLE + } else { + 0 + }) | (if flags & 0x04u8 != 0 { + Self::EXECUTABLE + } else { + 0 + }) | (if flags & 0x08u8 != 0 { + Self::ACCESSED + } else { + 0 + }) | (if flags & 0x10u8 != 0 { + Self::DIRTY + } else { + 0 + }) | (if flags & 0x40u8 != 0 { + Self::RSW1 + } else { + 0 + }) | (if flags & 0x80u8 != 0 { + Self::RSW2 + } else { + 0 + }) | (if priv_flags & 0x01u8 != 0 { + Self::USER + } else { + 0 + }) | (if priv_flags & 0x02u8 != 0 { + Self::GLOBAL + } else { + 0 + }) | (if cache is Uncacheable { + Self::PBMT_IO + } else { + 0 + }) + } + + pub open spec fn property_bits_spec(prop: PageProperty) -> usize { + Self::property_bits_from_parts_spec(prop.flags.bits(), prop.priv_flags.bits(), prop.cache) + } + + pub open spec fn decode_page_flags_spec(raw: usize) -> u8 { + (if raw & Self::READABLE != 0 { + 0x01u8 + } else { + 0 + }) | (if raw & Self::WRITABLE != 0 { + 0x02u8 + } else { + 0 + }) | (if raw & Self::EXECUTABLE != 0 { + 0x04u8 + } else { + 0 + }) | (if raw & Self::ACCESSED != 0 { + 0x08u8 + } else { + 0 + }) | (if raw & Self::DIRTY != 0 { + 0x10u8 + } else { + 0 + }) | (if raw & Self::RSW1 != 0 { + 0x40u8 + } else { + 0 + }) | (if raw & Self::RSW2 != 0 { + 0x80u8 + } else { + 0 + }) + } + + pub open spec fn decode_priv_flags_spec(raw: usize) -> u8 { + (if raw & Self::USER != 0 { + 0x01u8 + } else { + 0 + }) | (if raw & Self::GLOBAL != 0 { + 0x02u8 + } else { + 0 + }) + } + + pub open spec fn decode_cache_spec(raw: usize) -> CachePolicy { + if raw & Self::PBMT_IO != 0 { + CachePolicy::Uncacheable + } else { + CachePolicy::Writeback + } + } + + pub open spec fn prop_spec(self) -> PageProperty { + PageProperty { + flags: PageFlags::from_bits(Self::decode_page_flags_spec(self.raw))->0, + cache: Self::decode_cache_spec(self.raw), + priv_flags: PrivilegedPageFlags::from_bits(Self::decode_priv_flags_spec(self.raw))->0, + } + } + + pub open spec fn prop_from_raw_spec(raw: usize) -> PageProperty { + Self { raw }.prop_spec() + } + + pub open spec fn set_prop_req(prop: PageProperty) -> bool { + &&& prop.inv() + &&& (prop.cache is Writeback || prop.cache is Uncacheable) + &&& prop.flags.bits() & 0x07u8 != 0 + } + + pub open spec fn new_page_req(paddr: Paddr, level: PagingLevel, prop: PageProperty) -> bool { + &&& 1 <= level <= RiscvSv48PagingConsts::HIGHEST_TRANSLATION_LEVEL() + &&& paddr % RiscvSv48PagingConsts::BASE_PAGE_SIZE() == 0 + &&& paddr < RISCV_SV48_MAX_PADDR + &&& Self::set_prop_req(prop) + &&& (level == 1 || prop.flags.bits() & 0x07u8 != 0) + } + + pub open spec fn new_absent_spec() -> Self { + Self { raw: 0 } + } + + pub open spec fn new_pt_spec(paddr: Paddr) -> Self { + Self { raw: Self::paddr_bits(paddr) | Self::VALID } + } + + pub open spec fn new_page_spec(paddr: Paddr, prop: PageProperty) -> Self { + Self { raw: Self::paddr_bits(paddr) | Self::property_bits_spec(prop) } + } + + pub open spec fn set_prop_spec(self, prop: PageProperty) -> Self { + if self.is_present_spec() { + Self { raw: (self.raw & Self::PHYS_ADDR_MASK) | Self::property_bits_spec(prop) } + } else { + self + } + } + + pub open spec fn set_prop_raw_spec(old_raw: usize, prop: PageProperty) -> usize { + Self { raw: old_raw }.set_prop_spec(prop).raw + } +} + +#[verifier::bit_vector] +proof fn lemma_riscv_paddr_encoding_bv(paddr: usize) + requires + paddr % 4096usize == 0, + paddr < RISCV_SV48_MAX_PADDR, + ensures + ((((paddr >> 12) << 10) & RiscvPteModel::PHYS_ADDR_MASK) >> 10) << 12 == paddr, + ((paddr >> 12) << 10) & (RiscvPteModel::VALID | RiscvPteModel::READABLE + | RiscvPteModel::WRITABLE | RiscvPteModel::EXECUTABLE) == 0, +{ +} + +/// PPN encoding is lossless for aligned physical addresses representable by Sv48. +pub proof fn lemma_riscv_paddr_roundtrip(paddr: Paddr) + requires + paddr % 4096 == 0, + paddr < RISCV_SV48_MAX_PADDR, + ensures + RiscvPteModel::new_pt_spec(paddr).paddr_spec() == paddr, +{ + lemma_riscv_paddr_encoding_bv(paddr); + assert(RISCV_SV48_MAX_PADDR == 0x0100_0000_0000_0000usize) by (compute_only); + assert(paddr < 0x0100_0000_0000_0000usize); + assert(RiscvPteModel::new_pt_spec(paddr).raw == ((paddr >> 12) << 10) | 1usize) + by (compute_only); + assert(RiscvPteModel::new_pt_spec(paddr).paddr_spec() == paddr) by { + assert(((((paddr >> 12) << 10) | 1usize) & RiscvPteModel::PHYS_ADDR_MASK) == (((paddr >> 12) + << 10) & RiscvPteModel::PHYS_ADDR_MASK)) by (bit_vector); + } +} + +/// A child-table PTE is valid, has no RWX bits, and is never a leaf. +pub proof fn lemma_riscv_new_pt_shape(paddr: Paddr) + requires + paddr % 4096 == 0, + paddr < RISCV_SV48_MAX_PADDR, + ensures + RiscvPteModel::new_pt_spec(paddr).is_present_spec(), + forall|level: PagingLevel| !RiscvPteModel::new_pt_spec(paddr).is_last_spec(level), +{ + lemma_riscv_paddr_encoding_bv(paddr); + assert(RISCV_SV48_MAX_PADDR == 0x0100_0000_0000_0000usize) by (compute_only); + assert(paddr < 0x0100_0000_0000_0000usize); + assert(RiscvPteModel::new_pt_spec(paddr).is_present_spec()) by (bit_vector); + assert(RiscvPteModel::new_pt_spec(paddr).raw == ((paddr >> 12) << 10) | 1usize) + by (compute_only); + assert(((paddr >> 12) << 10) & (RiscvPteModel::READABLE | RiscvPteModel::WRITABLE + | RiscvPteModel::EXECUTABLE) == 0) by (bit_vector) + requires + paddr < 0x0100_0000_0000_0000usize, + paddr % 4096usize == 0, + ; + assert(RiscvPteModel::new_pt_spec(paddr).raw & (RiscvPteModel::READABLE + | RiscvPteModel::WRITABLE | RiscvPteModel::EXECUTABLE) == 0) by (bit_vector) + requires + RiscvPteModel::new_pt_spec(paddr).raw == ((paddr >> 12) << 10) | 1usize, + ((paddr >> 12) << 10) & (RiscvPteModel::READABLE | RiscvPteModel::WRITABLE + | RiscvPteModel::EXECUTABLE) == 0, + ; + assert forall|level: PagingLevel| !RiscvPteModel::new_pt_spec(paddr).is_last_spec(level) by { + assert(!RiscvPteModel::new_pt_spec(paddr).is_last_spec(level)); + } +} + +} // verus! diff --git a/ostd/specs/arch/x86/mod.rs b/ostd/specs/arch/x86/mod.rs index af7bd7a88..7398275b1 100644 --- a/ostd/specs/arch/x86/mod.rs +++ b/ostd/specs/arch/x86/mod.rs @@ -3,13 +3,17 @@ use vstd::prelude::*; use vstd::arithmetic::power2::{lemma_pow2_adds, lemma2_to64, lemma2_to64_rest, pow2}; use vstd_extra::prelude::*; +#[path = "../model.rs"] +pub mod model; +pub use model::*; + use crate::specs::mm::{ frame::mapping::lemma_meta_to_frame_soundness, page_table::{nr_pte_index_bits_spec, pte_index_bit_offset_spec}, }; use crate::mm::{ - Paddr, PagingConstsTrait, Vaddr, + CurrentPagingConstsTrait, Paddr, PagingConstsTrait, PagingLevel, Vaddr, frame::meta::{META_SLOT_SIZE, mapping::meta_to_frame}, kspace::{FRAME_METADATA_RANGE, LINEAR_MAPPING_BASE_VADDR, VMALLOC_BASE_VADDR, paddr_to_vaddr}, page_size, @@ -43,16 +47,64 @@ pub open spec fn valid_frame_paddr(paddr: Paddr) -> bool { &&& paddr < MAX_PADDR } -} // verus! -verus! { +/// The x86 instance of the architecture-wide specification contract. +pub struct X86Arch; + +impl ArchPagingModel for X86Arch { + type C = crate::arch::mm::PagingConsts; + + open spec fn max_paddr_spec() -> Paddr { + MAX_PADDR + } + + proof fn lemma_paging_model_requirements() { + Self::C::lemma_paging_consts_requirements(); + + } +} + +impl ArchAddressSpaceModel for X86Arch { + open spec fn linear_mapping_base_vaddr_spec() -> Vaddr { + LINEAR_MAPPING_BASE_VADDR + } + + open spec fn vmalloc_base_vaddr_spec() -> Vaddr { + VMALLOC_BASE_VADDR + } + + proof fn lemma_address_space_model_requirements() { + Self::C::lemma_paging_consts_requirements(); + Self::lemma_paging_model_requirements(); + assert(Self::linear_mapping_base_vaddr_spec() % Self::C::BASE_PAGE_SIZE() == 0) + by (compute_only); + + assert(Self::max_paddr_spec() < Self::vmalloc_base_vaddr_spec() + - Self::linear_mapping_base_vaddr_spec()) by (compute_only); + + } +} + +impl ArchTrait for X86Arch { + +} + +/// The architecture selected by the current verification target. +pub type CurrentArch = X86Arch; + +pub proof fn lemma_valid_frame_paddr_model_equivalent(paddr: Paddr) + ensures + valid_frame_paddr(paddr) == model::valid_frame_paddr_for::(paddr), +{ + CurrentArch::lemma_paging_model_requirements(); +} pub proof fn lemma_linear_mapping_base_vaddr_properties() ensures LINEAR_MAPPING_BASE_VADDR % PAGE_SIZE == 0, LINEAR_MAPPING_BASE_VADDR < VMALLOC_BASE_VADDR, { - assert(LINEAR_MAPPING_BASE_VADDR % PAGE_SIZE == 0) by (compute_only); - assert(LINEAR_MAPPING_BASE_VADDR < VMALLOC_BASE_VADDR) by (compute_only); + CurrentArch::lemma_address_space_model_requirements(); + } /// There is not an executable version in the source code. @@ -61,7 +113,7 @@ pub open spec fn vaddr_to_paddr(va: Vaddr) -> usize recommends LINEAR_MAPPING_BASE_VADDR <= va < VMALLOC_BASE_VADDR, { - (va - LINEAR_MAPPING_BASE_VADDR) as usize + model::vaddr_to_paddr_for::(va) } pub broadcast proof fn lemma_paddr_to_vaddr_properties(pa: Paddr) @@ -87,8 +139,8 @@ pub proof fn lemma_max_paddr_range() MAX_PADDR < VMALLOC_BASE_VADDR - LINEAR_MAPPING_BASE_VADDR, MAX_PADDR + LINEAR_MAPPING_BASE_VADDR < usize::MAX, { - assert(MAX_PADDR < VMALLOC_BASE_VADDR - LINEAR_MAPPING_BASE_VADDR) by (compute_only); - assert(MAX_PADDR + LINEAR_MAPPING_BASE_VADDR < usize::MAX) by (compute_only); + CurrentArch::lemma_address_space_model_requirements(); + } pub broadcast proof fn lemma_meta_frame_vaddr_properties(meta: Vaddr) @@ -113,7 +165,7 @@ pub broadcast proof fn lemma_meta_frame_vaddr_properties(meta: Vaddr) // Here are some architecture-specific const value properties. // Any use of this lemma in architecture-independent code should be removed. -pub(crate) proof fn lemma_arch_specific_consts_properties() +pub(crate) proof fn lemma_arch_specific_consts_properties() ensures C::BASE_PAGE_SIZE().ilog2() == 12u32, nr_pte_index_bits_spec::() == 9usize, @@ -127,6 +179,7 @@ pub(crate) proof fn lemma_arch_specific_consts_properties( 0xffff_int * 0x1_0000_0000_0000int + pow2(48) - 1 == 0xffff_ffff_ffff_ffffint, { C::lemma_paging_consts_properties(); + C::lemma_current_paging_consts_requirements(); lemma2_to64(); lemma2_to64_rest(); lemma_usize_pow2_ilog2(12); @@ -136,4 +189,17 @@ pub(crate) proof fn lemma_arch_specific_consts_properties( lemma_pow2_adds(8, 39); } +/// Verification-root regression for the RISC-V Sv48 paging/PTE model. +pub proof fn lemma_riscv_sv48_model_regression(paddr: Paddr) + requires + paddr % 4096 == 0, + paddr < crate::specs::riscv_arch::RISCV_SV48_MAX_PADDR, + ensures + crate::specs::riscv_arch::RiscvPteModel::new_pt_spec(paddr).paddr_spec() == paddr, +{ + crate::specs::riscv_arch::RiscvSv48PagingConsts::lemma_paging_consts_properties(); + crate::specs::riscv_arch::RiscvPagingModel::lemma_paging_model_requirements(); + crate::specs::riscv_arch::lemma_riscv_paddr_roundtrip(paddr); +} + } // verus! diff --git a/ostd/specs/mm/page_table/cursor/owners.rs b/ostd/specs/mm/page_table/cursor/owners.rs index 487043fe6..4c2b3cd68 100644 --- a/ostd/specs/mm/page_table/cursor/owners.rs +++ b/ostd/specs/mm/page_table/cursor/owners.rs @@ -34,7 +34,7 @@ use crate::specs::{ use crate::arch::mm::PagingConsts; use crate::mm::{ - MAX_USERSPACE_VADDR, Paddr, PagingConstsTrait, PagingLevel, Vaddr, + CurrentPagingConstsTrait, MAX_USERSPACE_VADDR, Paddr, PagingConstsTrait, PagingLevel, Vaddr, frame::meta::{REF_COUNT_MAX, REF_COUNT_UNIQUE, REF_COUNT_UNUSED}, kspace::KernelPtConfig, nr_subpage_per_huge, @@ -2369,6 +2369,7 @@ pub proof fn lemma_view_in_vaddr_range<'rcu, C: PageTableConfig>(owner: &CursorO }, { C::lemma_paging_consts_properties(); + C::lemma_current_paging_consts_requirements(); C::lemma_page_table_config_constant_properties(); lemma_arch_specific_consts_properties::(); diff --git a/ostd/specs/mod.rs b/ostd/specs/mod.rs index bc8234611..86f4570f2 100644 --- a/ostd/specs/mod.rs +++ b/ostd/specs/mod.rs @@ -10,6 +10,8 @@ pub mod arch; #[allow(rustdoc::invalid_rust_codeblocks)] #[allow(rustdoc::invalid_html_tags)] pub mod mm; +#[path = "arch/riscv/mod.rs"] +pub mod riscv_arch; #[allow(unused_parens)] #[allow(unused_braces)] mod sync; diff --git a/ostd/src/arch/riscv/mm/mod.rs b/ostd/src/arch/riscv/mm/mod.rs index 2b02cf27c..61f5e5200 100644 --- a/ostd/src/arch/riscv/mm/mod.rs +++ b/ostd/src/arch/riscv/mm/mod.rs @@ -1,92 +1,319 @@ // SPDX-License-Identifier: MPL-2.0 use alloc::fmt; use core::ops::Range; +use vstd::arithmetic::power2::*; +use vstd::prelude::*; +use vstd_extra::panic::{may_panic, panic_diverge}; +use vstd_extra::prelude::*; +use crate::specs::{ + arch::{valid_frame_paddr, MAX_PADDR, PAGE_SIZE}, + riscv_arch::RiscvPteModel, +}; use crate::{ - Pod, mm::{ - PAGE_SIZE, Paddr, PagingConstsTrait, PagingLevel, PodOnce, Vaddr, page_prop::{CachePolicy, PageFlags, PageProperty, PrivilegedPageFlags as PrivFlags}, page_table::PageTableEntryTrait, + Paddr, PagingConstsTrait, PagingLevel, PodOnce, Vaddr, }, + Pod, }; +verus! { + pub(crate) const NR_ENTRIES_PER_PAGE: usize = 512; +#[verifier::allow(autoderive_clone_without_spec)] #[derive(Clone, Debug, Default)] pub struct PagingConsts {} impl PagingConstsTrait for PagingConsts { - const BASE_PAGE_SIZE: usize = 4096; - const NR_LEVELS: PagingLevel = 4; - const ADDRESS_WIDTH: usize = 48; - const VA_SIGN_EXT: bool = true; - const HIGHEST_TRANSLATION_LEVEL: PagingLevel = 4; - const PTE_SIZE: usize = core::mem::size_of::(); + #[verifier::inline] + open spec fn BASE_PAGE_SIZE_spec() -> usize { + 4096 + } + + #[inline(always)] + fn BASE_PAGE_SIZE() -> usize { + 4096 + } + + #[verifier::inline] + open spec fn NR_LEVELS_spec() -> PagingLevel { + 4 + } + + #[inline(always)] + fn NR_LEVELS() -> PagingLevel { + 4 + } + + #[verifier::inline] + open spec fn ADDRESS_WIDTH_spec() -> usize { + 48 + } + + #[inline(always)] + fn ADDRESS_WIDTH() -> usize { + 48 + } + + #[verifier::inline] + open spec fn HIGHEST_TRANSLATION_LEVEL_spec() -> PagingLevel { + 4 + } + + #[inline(always)] + fn HIGHEST_TRANSLATION_LEVEL() -> PagingLevel { + 4 + } + + #[verifier::inline] + open spec fn VA_SIGN_EXT_spec() -> bool { + true + } + + #[inline(always)] + fn VA_SIGN_EXT() -> bool { + true + } + + #[verifier::inline] + open spec fn PTE_SIZE_spec() -> usize { + 8 + } + + #[inline(always)] + fn PTE_SIZE() -> usize { + 8 + } + + proof fn lemma_paging_consts_requirements() { + lemma_pow2_is_pow2_to64(); + lemma2_to64(); + lemma2_to64_rest(); + + vstd::layout::unsigned_int_max_values(); + vstd_extra::external::ilog2::lemma_usize_pow2_ilog2(9); + vstd_extra::external::ilog2::lemma_usize_pow2_ilog2(12); + lemma_pow2_adds(9, 39); + } +} + +pub(crate) proof fn lemma_nr_subpage_per_huge_eq_nr_entries() + ensures + crate::mm::nr_subpage_per_huge::() == NR_ENTRIES_PER_PAGE, +{ } -bitflags_upstream::bitflags! { - #[derive(Pod)] - #[repr(C)] +bitflags::bitflags! { /// Possible flags for a page table entry. pub struct PageTableFlags: usize { /// Specifies whether the mapped frame or page table is valid. - const VALID = 1 << 0; + const VALID = 1usize << 0; /// Controls whether reads to the mapped frames are allowed. - const READABLE = 1 << 1; + const READABLE = 1usize << 1; /// Controls whether writes to the mapped frames are allowed. - const WRITABLE = 1 << 2; + const WRITABLE = 1usize << 2; /// Controls whether execution code in the mapped frames are allowed. - const EXECUTABLE = 1 << 3; + const EXECUTABLE = 1usize << 3; /// Controls whether accesses from userspace (i.e. U-mode) are permitted. - const USER = 1 << 4; + const USER = 1usize << 4; /// Indicates that the mapping is present in all address spaces, so it isn't flushed from /// the TLB on an address space switch. - const GLOBAL = 1 << 5; + const GLOBAL = 1usize << 5; /// Whether the memory area represented by this entry is accessed. - const ACCESSED = 1 << 6; + const ACCESSED = 1usize << 6; /// Whether the memory area represented by this entry is modified. - const DIRTY = 1 << 7; + const DIRTY = 1usize << 7; // First bit ignored by MMU. - const RSV1 = 1 << 8; + const RSV1 = 1usize << 8; // Second bit ignored by MMU. - const RSV2 = 1 << 9; + const RSV2 = 1usize << 9; // PBMT: Non-cacheable, idempotent, weakly-ordered (RVWMO), main memory - const PBMT_NC = 1 << 61; + const PBMT_NC = 1usize << 61; // PBMT: Non-cacheable, non-idempotent, strongly-ordered (I/O ordering), I/O - const PBMT_IO = 1 << 62; + const PBMT_IO = 1usize << 62; /// Naturally aligned power-of-2 - const NAPOT = 1 << 63; + const NAPOT = 1usize << 63; } } +proof fn lemma_riscv_page_property_flag_constants() + ensures + PageTableFlags::VALID().bits() == 0x1usize, + PageTableFlags::READABLE().bits() == 0x2usize, + PageTableFlags::WRITABLE().bits() == 0x4usize, + PageTableFlags::EXECUTABLE().bits() == 0x8usize, + PageTableFlags::USER().bits() == 0x10usize, + PageTableFlags::GLOBAL().bits() == 0x20usize, + PageTableFlags::ACCESSED().bits() == 0x40usize, + PageTableFlags::DIRTY().bits() == 0x80usize, + PageTableFlags::RSV1().bits() == 0x100usize, + PageTableFlags::RSV2().bits() == 0x200usize, + PageTableFlags::PBMT_IO().bits() == 0x4000_0000_0000_0000usize, + PageTableFlags::VALID().bits().ilog2() == 0u32, + PageTableFlags::READABLE().bits().ilog2() == 1u32, + PageTableFlags::WRITABLE().bits().ilog2() == 2u32, + PageTableFlags::EXECUTABLE().bits().ilog2() == 3u32, + PageTableFlags::USER().bits().ilog2() == 4u32, + PageTableFlags::GLOBAL().bits().ilog2() == 5u32, + PageTableFlags::ACCESSED().bits().ilog2() == 6u32, + PageTableFlags::DIRTY().bits().ilog2() == 7u32, + PageTableFlags::RSV1().bits().ilog2() == 8u32, + PageTableFlags::RSV2().bits().ilog2() == 9u32, + PageFlags::R().bits() == 0x1u8, + PageFlags::W().bits() == 0x2u8, + PageFlags::X().bits() == 0x4u8, + PageFlags::ACCESSED().bits() == 0x8u8, + PageFlags::DIRTY().bits() == 0x10u8, + PageFlags::AVAIL1().bits() == 0x40u8, + PageFlags::AVAIL2().bits() == 0x80u8, + PageFlags::all().bits() == 0xDFu8, + PageFlags::R().bits().ilog2() == 0u32, + PageFlags::W().bits().ilog2() == 1u32, + PageFlags::X().bits().ilog2() == 2u32, + PageFlags::ACCESSED().bits().ilog2() == 3u32, + PageFlags::DIRTY().bits().ilog2() == 4u32, + PageFlags::AVAIL1().bits().ilog2() == 6u32, + PageFlags::AVAIL2().bits().ilog2() == 7u32, + PrivFlags::USER().bits() == 0x1u8, + PrivFlags::GLOBAL().bits() == 0x2u8, + PrivFlags::all().bits() == 0x3u8, + PrivFlags::USER().bits().ilog2() == 0u32, + PrivFlags::GLOBAL().bits().ilog2() == 1u32, +{ + lemma_usize_ilog2_to32(); + lemma_u8_ilog2_to8(); + broadcast use PageTableFlags::lemma_consts; + + PageTableFlags::lemma_all_constant(); + broadcast use PageFlags::lemma_consts; + broadcast use PrivFlags::lemma_consts; + + PageFlags::lemma_all_constant(); + PrivFlags::lemma_all_constant(); + assert(PageTableFlags::VALID().bits() == 0x1usize) by (compute); + assert(PageTableFlags::READABLE().bits() == 0x2usize) by (compute); + assert(PageTableFlags::WRITABLE().bits() == 0x4usize) by (compute); + assert(PageTableFlags::EXECUTABLE().bits() == 0x8usize) by (compute); + assert(PageTableFlags::USER().bits() == 0x10usize) by (compute); + assert(PageTableFlags::GLOBAL().bits() == 0x20usize) by (compute); + assert(PageTableFlags::ACCESSED().bits() == 0x40usize) by (compute); + assert(PageTableFlags::DIRTY().bits() == 0x80usize) by (compute); + assert(PageTableFlags::RSV1().bits() == 0x100usize) by (compute); + assert(PageTableFlags::RSV2().bits() == 0x200usize) by (compute); + assert(PageTableFlags::PBMT_IO().bits() == 0x4000_0000_0000_0000usize) by (compute); + + assert((0u8 | 0x1u8 | 0x2u8 | 0x4u8 | 0x3u8 | 0x5u8 | 0x7u8 | 0x8u8 | 0x10u8 | 0x40u8 | 0x80u8) + == 0xDFu8) by (bit_vector); + assert((0u8 | 0x1u8 | 0x2u8 | 0u8) == 0x3u8) by (bit_vector); +} + +} // verus! +#[cfg(target_arch = "riscv64")] pub(crate) fn tlb_flush_addr(vaddr: Vaddr) { unsafe { riscv::asm::sfence_vma(0, vaddr); } } +#[cfg(target_arch = "riscv64")] pub(crate) fn tlb_flush_addr_range(range: &Range) { for vaddr in range.clone().step_by(PAGE_SIZE) { tlb_flush_addr(vaddr); } } +#[cfg(target_arch = "riscv64")] pub(crate) fn tlb_flush_all_excluding_global() { // TODO: excluding global? riscv::asm::sfence_vma_all() } +#[cfg(target_arch = "riscv64")] pub(crate) fn tlb_flush_all_including_global() { riscv::asm::sfence_vma_all() } -#[derive(Clone, Copy, Pod, Default)] +verus! { + +#[derive(Clone, Copy)] #[repr(C)] pub struct PageTableEntry(usize); +global layout PageTableEntry is size == 8, align == 8; + +impl PageTableEntry { + pub const VALID_BIT: usize = 0x1; + + pub const READABLE_BIT: usize = 0x2; + + pub const WRITABLE_BIT: usize = 0x4; + + pub const EXECUTABLE_BIT: usize = 0x8; + + pub const USER_BIT: usize = 0x10; + + pub const GLOBAL_BIT: usize = 0x20; + + pub const ACCESSED_BIT: usize = 0x40; + + pub const DIRTY_BIT: usize = 0x80; + + pub const RSV1_BIT: usize = 0x100; + + pub const RSV2_BIT: usize = 0x200; + + pub const PBMT_IO_BIT: usize = 0x4000_0000_0000_0000; + + pub const PHYS_ADDR_MASK: usize = 0x003F_FFFF_FFFF_FC00; + + pub proof fn lemma_layout() + ensures + core::mem::size_of::() == 8, + core::mem::align_of::() == 8, + core::mem::size_of::() % core::mem::align_of::() == 0, + { + broadcast use VERUS_layout_of_PageTableEntry; + + } + + closed spec fn default_spec() -> Self { + Self(0) + } + + fn new_paddr(paddr: Paddr) -> Self { + let ppn = paddr >> 12; + Self(ppn << 10) + } + + #[inline(always)] + fn from_raw(raw: usize) -> (res: Self) + ensures + res.0 == raw, + { + Self(raw) + } +} + +#[verus_verify] +unsafe impl Pod for PageTableEntry { + +} + +impl Default for PageTableEntry { + fn default() -> (res: Self) + returns + Self::new_absent_spec(), + { + Self(0) + } +} + +} // verus! /// Activate the given level 4 page table. /// /// "satp" register doesn't have a field that encodes the cache policy, @@ -96,25 +323,18 @@ pub struct PageTableEntry(usize); /// /// Changing the level 4 page table is unsafe, because it's possible to violate memory safety by /// changing the page mapping. +#[cfg(target_arch = "riscv64")] pub unsafe fn activate_page_table(root_paddr: Paddr, _root_pt_cache: CachePolicy) { assert!(root_paddr % PagingConsts::BASE_PAGE_SIZE() == 0); let ppn = root_paddr >> 12; riscv::register::satp::set(riscv::register::satp::Mode::Sv48, 0, ppn); } +#[cfg(target_arch = "riscv64")] pub fn current_page_table_paddr() -> Paddr { riscv::register::satp::read().ppn() << 12 } -impl PageTableEntry { - const PHYS_ADDR_MASK: usize = 0x003F_FFFF_FFFF_FC00; - - fn new_paddr(paddr: Paddr) -> Self { - let ppn = paddr >> 12; - Self(ppn << 10) - } -} - /// Parse a bit-flag bits `val` in the representation of `from` to `to` in bits. macro_rules! parse_flags { ($val:expr, $from:expr, $to:expr) => { @@ -124,46 +344,727 @@ macro_rules! parse_flags { impl PodOnce for PageTableEntry {} +verus! { + +impl PageTableEntry { + #[verifier::inline] + pub open spec fn raw_property_bits_from_parts_spec( + page_bits: u8, + priv_bits: u8, + cache: CachePolicy, + ) -> usize { + Self::VALID_BIT | if page_bits & 0x01u8 != 0 { + Self::READABLE_BIT + } else { + 0usize + } | if page_bits & 0x02u8 != 0 { + Self::WRITABLE_BIT + } else { + 0usize + } | if page_bits & 0x04u8 != 0 { + Self::EXECUTABLE_BIT + } else { + 0usize + } | if page_bits & 0x08u8 != 0 { + Self::ACCESSED_BIT + } else { + 0usize + } | if page_bits & 0x10u8 != 0 { + Self::DIRTY_BIT + } else { + 0usize + } | if priv_bits & 0x01u8 != 0 { + Self::USER_BIT + } else { + 0usize + } | if priv_bits & 0x02u8 != 0 { + Self::GLOBAL_BIT + } else { + 0usize + } | if page_bits & 0x40u8 != 0 { + Self::RSV1_BIT + } else { + 0usize + } | if page_bits & 0x80u8 != 0 { + Self::RSV2_BIT + } else { + 0usize + } | if cache is Uncacheable { + Self::PBMT_IO_BIT + } else { + 0usize + } + } + + pub open spec fn raw_property_bits_spec(prop: PageProperty) -> usize { + Self::raw_property_bits_from_parts_spec( + prop.flags.bits(), + prop.priv_flags.bits(), + prop.cache, + ) + } + + pub open spec fn raw_set_prop_spec(old_raw: usize, prop: PageProperty) -> usize { + if old_raw & Self::VALID_BIT != 0 { + (old_raw & Self::PHYS_ADDR_MASK) | Self::raw_property_bits_spec(prop) + } else { + old_raw + } + } +} + +proof fn lemma_riscv_parse_flags(raw: usize) + ensures + parse_flags!(raw, PageTableFlags::READABLE(), PageFlags::R()) == if raw & 0x2usize != 0 { + 0x1usize + } else { + 0usize + }, + parse_flags!(raw, PageTableFlags::WRITABLE(), PageFlags::W()) == if raw & 0x4usize != 0 { + 0x2usize + } else { + 0usize + }, + parse_flags!(raw, PageTableFlags::EXECUTABLE(), PageFlags::X()) == if raw & 0x8usize != 0 { + 0x4usize + } else { + 0usize + }, + parse_flags!(raw, PageTableFlags::ACCESSED(), PageFlags::ACCESSED()) == if raw & 0x40usize + != 0 { + 0x8usize + } else { + 0usize + }, + parse_flags!(raw, PageTableFlags::DIRTY(), PageFlags::DIRTY()) == if raw & 0x80usize != 0 { + 0x10usize + } else { + 0usize + }, + parse_flags!(raw, PageTableFlags::RSV1(), PageFlags::AVAIL1()) == if raw & 0x100usize != 0 { + 0x40usize + } else { + 0usize + }, + parse_flags!(raw, PageTableFlags::RSV2(), PageFlags::AVAIL2()) == if raw & 0x200usize != 0 { + 0x80usize + } else { + 0usize + }, + parse_flags!(raw, PageTableFlags::USER(), PrivFlags::USER()) == if raw & 0x10usize != 0 { + 0x1usize + } else { + 0usize + }, + parse_flags!(raw, PageTableFlags::GLOBAL(), PrivFlags::GLOBAL()) == if raw & 0x20usize + != 0 { + 0x2usize + } else { + 0usize + }, +{ + lemma_riscv_page_property_flag_constants(); + assert(((raw & 0x2usize) >> 1 << 0) == (if raw & 0x2usize != 0 { + 0x1usize + } else { + 0usize + })) by (bit_vector); + assert(((raw & 0x4usize) >> 2 << 1) == (if raw & 0x4usize != 0 { + 0x2usize + } else { + 0usize + })) by (bit_vector); + assert(((raw & 0x8usize) >> 3 << 2) == (if raw & 0x8usize != 0 { + 0x4usize + } else { + 0usize + })) by (bit_vector); + assert(((raw & 0x40usize) >> 6 << 3) == (if raw & 0x40usize != 0 { + 0x8usize + } else { + 0usize + })) by (bit_vector); + assert(((raw & 0x80usize) >> 7 << 4) == (if raw & 0x80usize != 0 { + 0x10usize + } else { + 0usize + })) by (bit_vector); + assert(((raw & 0x100usize) >> 8 << 6) == (if raw & 0x100usize != 0 { + 0x40usize + } else { + 0usize + })) by (bit_vector); + assert(((raw & 0x200usize) >> 9 << 7) == (if raw & 0x200usize != 0 { + 0x80usize + } else { + 0usize + })) by (bit_vector); + assert(((raw & 0x10usize) >> 4 << 0) == (if raw & 0x10usize != 0 { + 0x1usize + } else { + 0usize + })) by (bit_vector); + assert(((raw & 0x20usize) >> 5 << 1) == (if raw & 0x20usize != 0 { + 0x2usize + } else { + 0usize + })) by (bit_vector); +} + +proof fn lemma_riscv_encode_flags(page_bits: u8, priv_bits: u8) + ensures + parse_flags!(page_bits, PageFlags::R(), PageTableFlags::READABLE()) == if page_bits & 0x1u8 + != 0 { + 0x2usize + } else { + 0usize + }, + parse_flags!(page_bits, PageFlags::W(), PageTableFlags::WRITABLE()) == if page_bits & 0x2u8 + != 0 { + 0x4usize + } else { + 0usize + }, + parse_flags!(page_bits, PageFlags::X(), PageTableFlags::EXECUTABLE()) == if page_bits + & 0x4u8 != 0 { + 0x8usize + } else { + 0usize + }, + parse_flags!(page_bits, PageFlags::ACCESSED(), PageTableFlags::ACCESSED()) == if page_bits + & 0x8u8 != 0 { + 0x40usize + } else { + 0usize + }, + parse_flags!(page_bits, PageFlags::DIRTY(), PageTableFlags::DIRTY()) == if page_bits + & 0x10u8 != 0 { + 0x80usize + } else { + 0usize + }, + parse_flags!(page_bits, PageFlags::AVAIL1(), PageTableFlags::RSV1()) == if page_bits + & 0x40u8 != 0 { + 0x100usize + } else { + 0usize + }, + parse_flags!(page_bits, PageFlags::AVAIL2(), PageTableFlags::RSV2()) == if page_bits + & 0x80u8 != 0 { + 0x200usize + } else { + 0usize + }, + parse_flags!(priv_bits, PrivFlags::USER(), PageTableFlags::USER()) == if priv_bits & 0x1u8 + != 0 { + 0x10usize + } else { + 0usize + }, + parse_flags!(priv_bits, PrivFlags::GLOBAL(), PageTableFlags::GLOBAL()) == if priv_bits + & 0x2u8 != 0 { + 0x20usize + } else { + 0usize + }, +{ + lemma_riscv_page_property_flag_constants(); + assert((((page_bits as usize) & 0x1usize) >> 0 << 1) == (if page_bits & 0x1u8 != 0 { + 0x2usize + } else { + 0usize + })) by (bit_vector); + assert((((page_bits as usize) & 0x2usize) >> 1 << 2) == (if page_bits & 0x2u8 != 0 { + 0x4usize + } else { + 0usize + })) by (bit_vector); + assert((((page_bits as usize) & 0x4usize) >> 2 << 3) == (if page_bits & 0x4u8 != 0 { + 0x8usize + } else { + 0usize + })) by (bit_vector); + assert((((page_bits as usize) & 0x8usize) >> 3 << 6) == (if page_bits & 0x8u8 != 0 { + 0x40usize + } else { + 0usize + })) by (bit_vector); + assert((((page_bits as usize) & 0x10usize) >> 4 << 7) == (if page_bits & 0x10u8 != 0 { + 0x80usize + } else { + 0usize + })) by (bit_vector); + assert((((page_bits as usize) & 0x40usize) >> 6 << 8) == (if page_bits & 0x40u8 != 0 { + 0x100usize + } else { + 0usize + })) by (bit_vector); + assert((((page_bits as usize) & 0x80usize) >> 7 << 9) == (if page_bits & 0x80u8 != 0 { + 0x200usize + } else { + 0usize + })) by (bit_vector); + assert((((priv_bits as usize) & 0x1usize) >> 0 << 4) == (if priv_bits & 0x1u8 != 0 { + 0x10usize + } else { + 0usize + })) by (bit_vector); + assert((((priv_bits as usize) & 0x2usize) >> 1 << 5) == (if priv_bits & 0x2u8 != 0 { + 0x20usize + } else { + 0usize + })) by (bit_vector); +} + +#[verifier::bit_vector] +proof fn lemma_riscv_property_bits_writeback(page_bits: u8, priv_bits: u8, flags: usize) + requires + flags == 0x1usize | if page_bits & 0x01u8 != 0 { + 0x2usize + } else { + 0usize + } | if page_bits & 0x02u8 != 0 { + 0x4usize + } else { + 0usize + } | if page_bits & 0x04u8 != 0 { + 0x8usize + } else { + 0usize + } | if page_bits & 0x08u8 != 0 { + 0x40usize + } else { + 0usize + } | if page_bits & 0x10u8 != 0 { + 0x80usize + } else { + 0usize + } | if priv_bits & 0x01u8 != 0 { + 0x10usize + } else { + 0usize + } | if priv_bits & 0x02u8 != 0 { + 0x20usize + } else { + 0usize + } | if page_bits & 0x40u8 != 0 { + 0x100usize + } else { + 0usize + } | if page_bits & 0x80u8 != 0 { + 0x200usize + } else { + 0usize + }, + ensures + flags == PageTableEntry::raw_property_bits_from_parts_spec( + page_bits, + priv_bits, + CachePolicy::Writeback, + ), +{ +} + +#[verifier::bit_vector] +proof fn lemma_riscv_property_bits_uncacheable(page_bits: u8, priv_bits: u8, flags: usize) + requires + flags == 0x1usize | if page_bits & 0x01u8 != 0 { + 0x2usize + } else { + 0usize + } | if page_bits & 0x02u8 != 0 { + 0x4usize + } else { + 0usize + } | if page_bits & 0x04u8 != 0 { + 0x8usize + } else { + 0usize + } | if page_bits & 0x08u8 != 0 { + 0x40usize + } else { + 0usize + } | if page_bits & 0x10u8 != 0 { + 0x80usize + } else { + 0usize + } | if priv_bits & 0x01u8 != 0 { + 0x10usize + } else { + 0usize + } | if priv_bits & 0x02u8 != 0 { + 0x20usize + } else { + 0usize + } | if page_bits & 0x40u8 != 0 { + 0x100usize + } else { + 0usize + } | if page_bits & 0x80u8 != 0 { + 0x200usize + } else { + 0usize + } | 0x4000_0000_0000_0000usize, + ensures + flags == PageTableEntry::raw_property_bits_from_parts_spec( + page_bits, + priv_bits, + CachePolicy::Uncacheable, + ), +{ +} + +#[verifier::bit_vector] +proof fn lemma_riscv_set_prop_bits_writeback( + old_raw: usize, + new_raw: usize, + page_bits: u8, + priv_bits: u8, +) + requires + page_bits & 0xDFu8 == page_bits, + priv_bits & 0x3u8 == priv_bits, + page_bits & 0x07u8 != 0, + new_raw == (old_raw & PageTableEntry::PHYS_ADDR_MASK) + | PageTableEntry::raw_property_bits_from_parts_spec( + page_bits, + priv_bits, + CachePolicy::Writeback, + ), + ensures + RiscvPteModel::paddr_from_raw_spec(new_raw) == RiscvPteModel::paddr_from_raw_spec(old_raw), + RiscvPteModel::decode_page_flags_spec(new_raw) == page_bits, + RiscvPteModel::decode_priv_flags_spec(new_raw) == priv_bits, + new_raw & PageTableEntry::VALID_BIT != 0, + new_raw & (PageTableEntry::READABLE_BIT | PageTableEntry::WRITABLE_BIT + | PageTableEntry::EXECUTABLE_BIT) != 0, + new_raw & PageTableEntry::PBMT_IO_BIT == 0, +{ +} + +#[verifier::bit_vector] +proof fn lemma_riscv_set_prop_bits_uncacheable( + old_raw: usize, + new_raw: usize, + page_bits: u8, + priv_bits: u8, +) + requires + page_bits & 0xDFu8 == page_bits, + priv_bits & 0x3u8 == priv_bits, + page_bits & 0x07u8 != 0, + new_raw == (old_raw & PageTableEntry::PHYS_ADDR_MASK) + | PageTableEntry::raw_property_bits_from_parts_spec( + page_bits, + priv_bits, + CachePolicy::Uncacheable, + ), + ensures + RiscvPteModel::paddr_from_raw_spec(new_raw) == RiscvPteModel::paddr_from_raw_spec(old_raw), + RiscvPteModel::decode_page_flags_spec(new_raw) == page_bits, + RiscvPteModel::decode_priv_flags_spec(new_raw) == priv_bits, + new_raw & PageTableEntry::VALID_BIT != 0, + new_raw & (PageTableEntry::READABLE_BIT | PageTableEntry::WRITABLE_BIT + | PageTableEntry::EXECUTABLE_BIT) != 0, + new_raw & PageTableEntry::PBMT_IO_BIT != 0, +{ +} + +proof fn lemma_riscv_set_prop_roundtrip(old_raw: usize, new_raw: usize, prop: PageProperty) + requires + prop.inv(), + prop.cache is Writeback || prop.cache is Uncacheable, + prop.flags.bits() & 0x07u8 != 0, + new_raw == PageTableEntry::raw_set_prop_spec(old_raw, prop), + old_raw & PageTableEntry::VALID_BIT != 0, + ensures + PageTableEntry(new_raw).prop() == prop, + PageTableEntry(new_raw).paddr() == PageTableEntry(old_raw).paddr(), + PageTableEntry(new_raw).is_present(), + forall|level: PagingLevel| PageTableEntry(new_raw).is_last(level), + forall|level: PagingLevel| #[trigger] + PageTableEntry(old_raw).is_last(level) ==> PageTableEntry(new_raw).is_last(level), +{ + lemma_riscv_page_property_flag_constants(); + let page_bits = prop.flags.bits(); + let priv_bits = prop.priv_flags.bits(); + + assert(new_raw == (old_raw & PageTableEntry::PHYS_ADDR_MASK) + | PageTableEntry::raw_property_bits_spec(prop)); + assert(PageTableEntry::raw_property_bits_spec(prop) + == PageTableEntry::raw_property_bits_from_parts_spec(page_bits, priv_bits, prop.cache)); + match prop.cache { + CachePolicy::Writeback => { + lemma_riscv_set_prop_bits_writeback(old_raw, new_raw, page_bits, priv_bits); + assert(RiscvPteModel::decode_cache_spec(new_raw) == CachePolicy::Writeback); + }, + CachePolicy::Uncacheable => { + lemma_riscv_set_prop_bits_uncacheable(old_raw, new_raw, page_bits, priv_bits); + assert(RiscvPteModel::decode_cache_spec(new_raw) == CachePolicy::Uncacheable); + }, + _ => {}, + } + assert(PageTableEntry(new_raw).paddr() == RiscvPteModel::paddr_from_raw_spec(new_raw)) + by (compute_only); + assert(PageTableEntry(old_raw).paddr() == RiscvPteModel::paddr_from_raw_spec(old_raw)) + by (compute_only); + assert(PageTableEntry(new_raw).is_present() == (new_raw & PageTableEntry::VALID_BIT != 0)) + by (compute_only); + assert(PageTableEntry(new_raw).is_present()); + assert(RiscvPteModel::decode_page_flags_spec(new_raw) == page_bits); + assert(RiscvPteModel::decode_priv_flags_spec(new_raw) == priv_bits); + PageFlags::lemma_from_bits_bits(page_bits); + PrivFlags::lemma_from_bits_bits(priv_bits); + PageFlags::lemma_eq_from_bits(PageTableEntry(new_raw).prop().flags, prop.flags); + PrivFlags::lemma_eq_from_bits(PageTableEntry(new_raw).prop().priv_flags, prop.priv_flags); + assert(PageTableEntry(new_raw).prop().cache == prop.cache); + assert(PageTableEntry(new_raw).prop() == prop); + assert forall|level: PagingLevel| PageTableEntry(new_raw).is_last(level) by { + assert(PageTableEntry(new_raw).is_last(level)); + } + assert forall|level: PagingLevel| #[trigger] + PageTableEntry(old_raw).is_last(level) implies PageTableEntry(new_raw).is_last(level) by { + assert(PageTableEntry(new_raw).is_last(level)); + } +} + +#[verifier::bit_vector] +proof fn lemma_riscv_decoded_flags_wf(raw: usize) + ensures + (RiscvPteModel::decode_page_flags_spec(raw) as usize) & 0xDFusize + == RiscvPteModel::decode_page_flags_spec(raw) as usize, + (RiscvPteModel::decode_priv_flags_spec(raw) as usize) & 0x3usize + == RiscvPteModel::decode_priv_flags_spec(raw) as usize, + RiscvPteModel::decode_page_flags_spec(raw) as usize <= 0xFFusize, + RiscvPteModel::decode_priv_flags_spec(raw) as usize <= 0xFFusize, +{ +} + +#[verifier::bit_vector] +proof fn lemma_riscv_paddr_encoding_for_current(paddr: Paddr) + requires + paddr < MAX_PADDR, + ensures + RiscvPteModel::paddr_from_raw_spec((paddr >> 12) << 10) == paddr & !((PAGE_SIZE + - 1) as usize), + valid_frame_paddr(RiscvPteModel::paddr_from_raw_spec((paddr >> 12) << 10)), +{ +} + impl PageTableEntryTrait for PageTableEntry { + fn new_absent() -> Self { + proof { + lemma_riscv_page_property_flag_constants(); + assert(Self::default_spec() == Self::new_absent_spec()) by (compute_only); + assert(0usize % PAGE_SIZE == 0) by (compute_only); + assert(0 < MAX_PADDR) by (compute_only); + assert(Self(0).paddr() == 0) by (compute_only); + assert(!Self(0).is_present()) by (bit_vector); + } + Self(0) + } + fn is_present(&self) -> bool { - self.0 & PageTableFlags::VALID.bits() != 0 + proof { + lemma_riscv_page_property_flag_constants(); + assert(self.is_present_spec() == (self.0 & 0x1usize != 0)) by (compute_only); + } + self.0 & PageTableFlags::VALID().bits() != 0 + } + + closed spec fn new_absent_spec() -> Self { + Self::default_spec() } - fn new_page(paddr: Paddr, _level: PagingLevel, prop: PageProperty) -> Self { - let mut pte = Self::new_paddr(paddr); + closed spec fn is_present_spec(&self) -> bool { + RiscvPteModel { raw: self.0 }.is_present_spec() + } + + closed spec fn new_page_spec(paddr: Paddr, _level: PagingLevel, prop: PageProperty) -> Self { + Self(Self::raw_set_prop_spec(((paddr >> 12) << 10) | Self::VALID_BIT, prop)) + } + + open spec fn new_page_req(paddr: Paddr, level: PagingLevel, prop: PageProperty) -> bool { + RiscvPteModel::new_page_req(paddr, level, prop) + } + + fn new_page(paddr: Paddr, level: PagingLevel, prop: PageProperty) -> Self { + let initial_pte = Self::from_raw(((paddr >> 12) << 10) | 1usize); + proof { + assert(Self::new_page_req(paddr, level, prop)); + assert(RiscvPteModel::new_page_req(paddr, level, prop)); + assert(paddr < MAX_PADDR); + assert(paddr % PAGE_SIZE == 0); + assert(initial_pte.0 == ((paddr >> 12) << 10) | 1usize); + let ghost initial_raw = initial_pte.as_usize(); + assert(initial_raw == ((paddr >> 12) << 10) | 1usize); + assert(initial_pte.paddr() == paddr & !((PAGE_SIZE - 1) as usize)) by { + lemma_riscv_paddr_encoding_for_current(paddr); + assert(initial_pte.paddr() == RiscvPteModel::paddr_from_raw_spec(initial_pte.0)) + by (compute_only); + assert(initial_pte.paddr() == RiscvPteModel::paddr_from_raw_spec(initial_raw)); + assert(RiscvPteModel::paddr_from_raw_spec(initial_raw) + == RiscvPteModel::paddr_from_raw_spec((paddr >> 12) << 10)) by (bit_vector) + requires + initial_raw == ((paddr >> 12) << 10) | 1usize, + ; + } + assert(paddr & !((PAGE_SIZE - 1) as usize) == paddr) by (bit_vector) + requires + paddr % PAGE_SIZE == 0, + ; + assert(initial_pte.paddr() == paddr); + assert(valid_frame_paddr(initial_pte.paddr())); + assert(initial_pte.0 == initial_raw); + assert(initial_pte.is_present() == (initial_pte.0 & Self::VALID_BIT != 0)) + by (compute_only); + assert(initial_raw & Self::VALID_BIT != 0) by (bit_vector) + requires + initial_raw == ((paddr >> 12) << 10) | 1usize, + ; + assert(initial_pte.is_present()); + } + let mut pte = initial_pte; pte.set_prop(prop); + proof { + lemma_riscv_paddr_encoding_for_current(paddr); + assert(pte.as_usize() == Self::raw_set_prop_spec( + ((paddr >> 12) << 10) | Self::VALID_BIT, + prop, + )); + assert(pte.as_usize() == Self::new_page_spec(paddr, level, prop).as_usize_spec()); + assert(pte == Self::new_page_spec(paddr, level, prop)); + assert(pte.is_present()); + assert(pte.prop() == prop); + assert(pte.paddr() == paddr & !((PAGE_SIZE - 1) as usize)); + assert(valid_frame_paddr(pte.paddr())); + assert(pte.is_last(level)); + } pte } + closed spec fn new_pt_spec(paddr: Paddr) -> Self { + Self(((paddr >> 12) << 10) | Self::VALID_BIT) + } + fn new_pt(paddr: Paddr) -> Self { // In RISC-V, non-leaf PTE should have RWX = 000, // and D, A, and U are reserved for future standard use. - let pte = Self::new_paddr(paddr); - PageTableEntry(pte.0 | PageTableFlags::VALID.bits()) + let pte = Self::from_raw((paddr >> 12) << 10); + let res = Self::from_raw(pte.0 | Self::VALID_BIT); + proof { + lemma_riscv_paddr_encoding_for_current(paddr); + assert(res.as_usize() == ((paddr >> 12) << 10) | Self::VALID_BIT); + assert(res.as_usize() == Self::new_pt_spec(paddr).as_usize_spec()); + assert(res == Self::new_pt_spec(paddr)); + let ghost res_raw = res.as_usize(); + assert(res_raw == ((paddr >> 12) << 10) | Self::VALID_BIT); + assert(res.paddr() == RiscvPteModel::paddr_from_raw_spec(res.0)) by (compute_only); + assert(res.0 == res_raw); + assert(RiscvPteModel::paddr_from_raw_spec(res_raw) + == RiscvPteModel::paddr_from_raw_spec((paddr >> 12) << 10)) by (bit_vector) + requires + res_raw == ((paddr >> 12) << 10) | Self::VALID_BIT, + ; + assert(RiscvPteModel::paddr_from_raw_spec((paddr >> 12) << 10) == paddr & !((PAGE_SIZE + - 1) as usize)); + assert(res.paddr() == paddr & !((PAGE_SIZE - 1) as usize)); + assert(paddr % PAGE_SIZE == 0 ==> res.paddr() == paddr) by { + if paddr % PAGE_SIZE == 0 { + assert(paddr & !((PAGE_SIZE - 1) as usize) == paddr) by (bit_vector) + requires + PAGE_SIZE == 4096usize, + paddr % PAGE_SIZE == 0, + ; + assert(res.paddr() == paddr); + } + } + assert(valid_frame_paddr(res.paddr())); + assert(res.is_present() == (res.0 & Self::VALID_BIT != 0)) by (compute_only); + assert(res_raw & Self::VALID_BIT != 0) by (bit_vector) + requires + res_raw == ((paddr >> 12) << 10) | Self::VALID_BIT, + ; + assert(res.0 & Self::VALID_BIT != 0); + assert(res_raw & Self::VALID_BIT != 0) by (bit_vector) + requires + res_raw == ((paddr >> 12) << 10) | Self::VALID_BIT, + ; + assert(res.is_present()); + assert forall|level: PagingLevel| !res.is_last(level) by { + assert(res_raw & 0xEusize == 0usize) by (bit_vector) + requires + res_raw == ((paddr >> 12) << 10) | Self::VALID_BIT, + ; + assert(res.as_usize() & 0xEusize == 0usize); + assert(res.is_last(level) == (res.as_usize() & 0xEusize != 0)) by (compute_only); + assert(!res.is_last(level)); + } + } + res + } + + closed spec fn paddr_spec(&self) -> Paddr { + RiscvPteModel { raw: self.0 }.paddr_spec() } fn paddr(&self) -> Paddr { + proof { + self.lemma_paddr_is_page_aligned(); + } let ppn = (self.0 & Self::PHYS_ADDR_MASK) >> 10; ppn << 12 } + closed spec fn prop_spec(&self) -> PageProperty { + RiscvPteModel { raw: self.0 }.prop_spec() + } + fn prop(&self) -> PageProperty { - let flags = (parse_flags!(self.0, PageTableFlags::READABLE, PageFlags::R)) - | (parse_flags!(self.0, PageTableFlags::WRITABLE, PageFlags::W)) - | (parse_flags!(self.0, PageTableFlags::EXECUTABLE, PageFlags::X)) - | (parse_flags!(self.0, PageTableFlags::ACCESSED, PageFlags::ACCESSED)) - | (parse_flags!(self.0, PageTableFlags::DIRTY, PageFlags::DIRTY)) - | (parse_flags!(self.0, PageTableFlags::RSV1, PageFlags::AVAIL1)) - | (parse_flags!(self.0, PageTableFlags::RSV2, PageFlags::AVAIL2)); - let priv_flags = (parse_flags!(self.0, PageTableFlags::USER, PrivFlags::USER)) - | (parse_flags!(self.0, PageTableFlags::GLOBAL, PrivFlags::GLOBAL)); - - let cache = if self.0 & PageTableFlags::PBMT_IO.bits() != 0 { + proof { + lemma_riscv_page_property_flag_constants(); + } + let flags = (parse_flags!(self.0, PageTableFlags::READABLE(), PageFlags::R())) | ( + parse_flags!(self.0, PageTableFlags::WRITABLE(), PageFlags::W())) | ( + parse_flags!(self.0, PageTableFlags::EXECUTABLE(), PageFlags::X())) | ( + parse_flags!(self.0, PageTableFlags::ACCESSED(), PageFlags::ACCESSED())) | ( + parse_flags!(self.0, PageTableFlags::DIRTY(), PageFlags::DIRTY())) | ( + parse_flags!(self.0, PageTableFlags::RSV1(), PageFlags::AVAIL1())) | ( + parse_flags!(self.0, PageTableFlags::RSV2(), PageFlags::AVAIL2())); + let priv_flags = (parse_flags!(self.0, PageTableFlags::USER(), PrivFlags::USER())) | ( + parse_flags!(self.0, PageTableFlags::GLOBAL(), PrivFlags::GLOBAL())); + + let cache = if self.0 & PageTableFlags::PBMT_IO().bits() != 0 { CachePolicy::Uncacheable } else { CachePolicy::Writeback }; + proof { + lemma_riscv_parse_flags(self.0); + lemma_riscv_decoded_flags_wf(self.0); + assert(flags == RiscvPteModel::decode_page_flags_spec(self.0) as usize); + assert(priv_flags == RiscvPteModel::decode_priv_flags_spec(self.0) as usize); + assert(flags & 0xDFusize == flags); + assert(priv_flags & 0x3usize == priv_flags); + assert(flags <= 0xFFusize); + assert(priv_flags <= 0xFFusize); + assert((flags as u8) & 0xDFu8 == flags as u8) by (bit_vector) + requires + flags & 0xDFusize == flags, + flags <= 0xFFusize, + ; + assert((priv_flags as u8) & 0x3u8 == priv_flags as u8) by (bit_vector) + requires + priv_flags & 0x3usize == priv_flags, + priv_flags <= 0xFFusize, + ; + assert((flags as u8) & PageFlags::all().bits() == flags as u8); + assert((priv_flags as u8) & PrivFlags::all().bits() == priv_flags as u8); + PageFlags::lemma_from_bits_bits(flags as u8); + PrivFlags::lemma_from_bits_bits(priv_flags as u8); + } + PageProperty { flags: PageFlags::from_bits(flags as u8).unwrap(), cache, @@ -171,42 +1072,319 @@ impl PageTableEntryTrait for PageTableEntry { } } - fn set_prop(&mut self, prop: PageProperty) { - let mut flags = PageTableFlags::VALID.bits() - | parse_flags!(prop.flags.bits(), PageFlags::R, PageTableFlags::READABLE) - | parse_flags!(prop.flags.bits(), PageFlags::W, PageTableFlags::WRITABLE) - | parse_flags!(prop.flags.bits(), PageFlags::X, PageTableFlags::EXECUTABLE) - | parse_flags!( - prop.priv_flags.bits(), - PrivFlags::USER, - PageTableFlags::USER - ) - | parse_flags!( - prop.priv_flags.bits(), - PrivFlags::GLOBAL, - PageTableFlags::GLOBAL - ) - | parse_flags!(prop.flags.bits(), PageFlags::AVAIL1, PageTableFlags::RSV1) - | parse_flags!(prop.flags.bits(), PageFlags::AVAIL2, PageTableFlags::RSV2); + open spec fn set_prop_req(self, prop: PageProperty) -> bool { + RiscvPteModel::set_prop_req(prop) + } + + fn set_prop(&mut self, prop: PageProperty) + ensures + old(self).is_present() ==> final(self).as_usize() == Self::raw_set_prop_spec( + old(self).as_usize(), + prop, + ), + old(self).is_present() ==> forall|level: PagingLevel| final(self).is_last(level), + { + proof { + lemma_riscv_page_property_flag_constants(); + } + if !self.is_present() { + return; + } + let page_bits = prop.flags.bits(); + let priv_bits = prop.priv_flags.bits(); + let base_flags = Self::VALID_BIT | if page_bits & 0x01u8 != 0 { + Self::READABLE_BIT + } else { + 0usize + } | if page_bits & 0x02u8 != 0 { + Self::WRITABLE_BIT + } else { + 0usize + } | if page_bits & 0x04u8 != 0 { + Self::EXECUTABLE_BIT + } else { + 0usize + } | if page_bits & 0x08u8 != 0 { + Self::ACCESSED_BIT + } else { + 0usize + } | if page_bits & 0x10u8 != 0 { + Self::DIRTY_BIT + } else { + 0usize + } | if priv_bits & 0x01u8 != 0 { + Self::USER_BIT + } else { + 0usize + } | if priv_bits & 0x02u8 != 0 { + Self::GLOBAL_BIT + } else { + 0usize + } | if page_bits & 0x40u8 != 0 { + Self::RSV1_BIT + } else { + 0usize + } | if page_bits & 0x80u8 != 0 { + Self::RSV2_BIT + } else { + 0usize + }; + let mut flags = base_flags; + proof { + lemma_riscv_encode_flags(page_bits, priv_bits); + assert(page_bits == prop.flags.bits()); + assert(priv_bits == prop.priv_flags.bits()); + } match prop.cache { - CachePolicy::Writeback => (), + CachePolicy::Writeback => { + proof { + reveal(PageTableEntry::raw_property_bits_spec); + assert(prop.cache is Writeback); + assert(!(prop.cache is Uncacheable)); + assert((if prop.cache is Uncacheable { + Self::PBMT_IO_BIT + } else { + 0usize + }) == 0usize); + assert(flags == base_flags); + lemma_riscv_property_bits_writeback(page_bits, priv_bits, flags); + assert(Self::raw_property_bits_from_parts_spec( + page_bits, + priv_bits, + CachePolicy::Writeback, + ) == Self::raw_property_bits_from_parts_spec(page_bits, priv_bits, prop.cache)); + assert(Self::raw_property_bits_from_parts_spec(page_bits, priv_bits, prop.cache) + == Self::raw_property_bits_spec(prop)); + } + }, CachePolicy::Uncacheable => { // Currently, Asterinas uses `Uncacheable` for I/O memory. - flags |= PageTableFlags::PBMT_IO.bits() - } - _ => panic!("unsupported cache policy"), + flags |= Self::PBMT_IO_BIT; + proof { + reveal(PageTableEntry::raw_property_bits_spec); + assert(prop.cache is Uncacheable); + assert(flags == base_flags | Self::PBMT_IO_BIT); + lemma_riscv_property_bits_uncacheable(page_bits, priv_bits, flags); + assert(Self::raw_property_bits_from_parts_spec( + page_bits, + priv_bits, + CachePolicy::Uncacheable, + ) == Self::raw_property_bits_from_parts_spec(page_bits, priv_bits, prop.cache)); + assert(Self::raw_property_bits_from_parts_spec(page_bits, priv_bits, prop.cache) + == Self::raw_property_bits_spec(prop)); + } + }, + _ => panic_diverge(), } self.0 = (self.0 & Self::PHYS_ADDR_MASK) | flags; + proof { + reveal(PageTableEntry::raw_set_prop_spec); + assert(old(self).is_present()); + match prop.cache { + CachePolicy::Writeback => { + lemma_riscv_property_bits_writeback(page_bits, priv_bits, flags); + assert(Self::raw_property_bits_from_parts_spec( + page_bits, + priv_bits, + CachePolicy::Writeback, + ) == Self::raw_property_bits_spec(prop)); + }, + CachePolicy::Uncacheable => { + lemma_riscv_property_bits_uncacheable(page_bits, priv_bits, flags); + assert(Self::raw_property_bits_from_parts_spec( + page_bits, + priv_bits, + CachePolicy::Uncacheable, + ) == Self::raw_property_bits_spec(prop)); + }, + _ => {}, + } + assert(flags == Self::raw_property_bits_spec(prop)); + assert(self.as_usize() == (old(self).as_usize() & Self::PHYS_ADDR_MASK) | flags); + assert(self.as_usize() == Self::raw_set_prop_spec(old(self).as_usize(), prop)); + lemma_riscv_set_prop_roundtrip(old(self).as_usize(), self.as_usize(), prop); + } + } + + closed spec fn is_last_spec(&self, level: PagingLevel) -> bool { + RiscvPteModel { raw: self.0 }.is_last_spec(level) } fn is_last(&self, level: PagingLevel) -> bool { - let rwx = PageTableFlags::READABLE | PageTableFlags::WRITABLE | PageTableFlags::EXECUTABLE; - level == 1 || (self.0 & rwx.bits()) != 0 + proof { + lemma_riscv_page_property_flag_constants(); + assert(self.is_last_spec(level) == (self.0 & 0xEusize != 0)) by (compute_only); + } + let rwx = PageTableFlags::READABLE() | PageTableFlags::WRITABLE() + | PageTableFlags::EXECUTABLE(); + (self.0 & rwx.bits()) != 0 + } + + closed spec fn as_usize_spec(self) -> usize { + self.0 + } + + fn as_usize(self) -> usize { + self.0 } + + fn from_usize(pte_raw: usize) -> Self { + Self(pte_raw) + } + + proof fn lemma_page_table_entry_properties() { + lemma_riscv_page_property_flag_constants(); + Self::lemma_layout(); + assert(core::mem::size_of::() == 8); + assert(core::mem::align_of::() == 8); + assert(8usize % 8usize == 0) by (compute_only); + assert(valid_frame_paddr(Self::new_absent().paddr())) by (compute_only); + assert(!Self::new_absent().is_present()) by (compute_only); + assert forall|level: PagingLevel| + #![trigger Self::new_absent().is_last(level)] + 1 < level ==> !Self::new_absent().is_last(level) by { + assert(!Self::new_absent().is_last(level)) by (compute_only); + } + assert forall|paddr: Paddr, level: PagingLevel, prop: PageProperty| + #![trigger Self::new_page(paddr, level, prop)] + Self::new_page_req(paddr, level, prop) && (prop.cache is Writeback + || prop.cache is Writethrough || prop.cache is Uncacheable) ==> { + &&& Self::new_page(paddr, level, prop).is_present() + &&& (paddr < MAX_PADDR ==> Self::new_page(paddr, level, prop).paddr() == paddr & !(( + PAGE_SIZE - 1) as usize)) + &&& (paddr < MAX_PADDR && paddr % PAGE_SIZE == 0 ==> Self::new_page( + paddr, + level, + prop, + ).paddr() == paddr) + &&& Self::new_page(paddr, level, prop).prop() == prop + &&& Self::new_page(paddr, level, prop).is_last(level) + } by { + if Self::new_page_req(paddr, level, prop) && (prop.cache is Writeback + || prop.cache is Writethrough || prop.cache is Uncacheable) { + let old_raw = ((paddr >> 12) << 10) | Self::VALID_BIT; + let pte = Self::new_page(paddr, level, prop); + let raw = pte.as_usize(); + reveal(::new_page_req); + assert(Self::new_page_req(paddr, level, prop)); + assert(prop.inv()); + assert(prop.cache is Writeback || prop.cache is Uncacheable); + assert(prop.flags.bits() & 0x07u8 != 0); + assert(pte.0 == raw); + reveal(::new_page_spec); + reveal(PageTableEntry::raw_set_prop_spec); + assert(pte.0 == Self::raw_set_prop_spec(old_raw, prop)); + assert(raw == Self::raw_set_prop_spec(old_raw, prop)); + assert(Self::VALID_BIT == 1usize) by (compute_only); + assert(old_raw & Self::VALID_BIT != 0) by (bit_vector) + requires + old_raw == ((paddr >> 12) << 10) | Self::VALID_BIT, + Self::VALID_BIT == 1usize, + ; + lemma_riscv_set_prop_roundtrip(old_raw, raw, prop); + assert(pte == PageTableEntry(raw)); + assert(pte.is_present()); + assert(pte.prop() == prop); + assert(pte.is_last(level)); + if paddr < MAX_PADDR { + lemma_riscv_paddr_encoding_for_current(paddr); + assert(PageTableEntry(old_raw).paddr() == RiscvPteModel::paddr_from_raw_spec( + old_raw, + )) by (compute_only); + assert(RiscvPteModel::paddr_from_raw_spec(old_raw) + == RiscvPteModel::paddr_from_raw_spec((paddr >> 12) << 10)) by (bit_vector) + requires + old_raw == ((paddr >> 12) << 10) | Self::VALID_BIT, + ; + assert(PageTableEntry(old_raw).paddr() == paddr & !((PAGE_SIZE - 1) as usize)); + assert(pte.paddr() == paddr & !((PAGE_SIZE - 1) as usize)); + if paddr % PAGE_SIZE == 0 { + assert(paddr & !((PAGE_SIZE - 1) as usize) == paddr) by (bit_vector) + requires + PAGE_SIZE == 4096usize, + paddr % PAGE_SIZE == 0, + ; + assert(pte.paddr() == paddr); + } + } + } + } + assert forall|paddr: Paddr| + #![trigger Self::new_pt(paddr)] + { + &&& Self::new_pt(paddr).is_present() + &&& (paddr < MAX_PADDR ==> Self::new_pt(paddr).paddr() == paddr & !((PAGE_SIZE + - 1) as usize)) + &&& (paddr < MAX_PADDR && paddr % PAGE_SIZE == 0 ==> Self::new_pt(paddr).paddr() + == paddr) + &&& forall|level: PagingLevel| !Self::new_pt(paddr).is_last(level) + } by { + let pte = Self::new_pt(paddr); + let raw = pte.as_usize(); + reveal(::new_pt_spec); + reveal(::as_usize_spec); + assert(pte.0 == ((paddr >> 12) << 10) | Self::VALID_BIT); + assert(raw == pte.0); + assert(raw == ((paddr >> 12) << 10) | Self::VALID_BIT); + assert(pte == PageTableEntry(raw)); + assert(raw & Self::VALID_BIT != 0) by (bit_vector) + requires + raw == ((paddr >> 12) << 10) | Self::VALID_BIT, + ; + reveal(::is_present_spec); + assert(pte.is_present() == (raw & Self::VALID_BIT != 0)); + assert(pte.is_present()); + assert(raw & 0xEusize == 0) by (bit_vector) + requires + raw == ((paddr >> 12) << 10) | Self::VALID_BIT, + ; + assert forall|level: PagingLevel| !pte.is_last(level) by { + reveal(::is_last_spec); + assert(pte.is_last(level) == (pte.0 & 0xEusize != 0)) by (compute_only); + assert(pte.0 == raw); + assert(pte.is_last(level) == (raw & 0xEusize != 0)); + assert(!pte.is_last(level)); + } + if paddr < MAX_PADDR { + lemma_riscv_paddr_encoding_for_current(paddr); + reveal(::paddr_spec); + assert(pte.paddr() == RiscvPteModel::paddr_from_raw_spec(raw)); + assert(RiscvPteModel::paddr_from_raw_spec(raw) + == RiscvPteModel::paddr_from_raw_spec((paddr >> 12) << 10)) by (bit_vector) + requires + raw == ((paddr >> 12) << 10) | Self::VALID_BIT, + ; + assert(pte.paddr() == paddr & !((PAGE_SIZE - 1) as usize)); + if paddr % PAGE_SIZE == 0 { + assert(paddr & !((PAGE_SIZE - 1) as usize) == paddr) by (bit_vector) + requires + PAGE_SIZE == 4096usize, + paddr % PAGE_SIZE == 0, + ; + assert(pte.paddr() == paddr); + } + } + } + } + + proof fn lemma_paddr_is_page_aligned(self) { + assert(self.paddr() == RiscvPteModel { raw: self.0 }.paddr_spec()) by (compute_only); + lemma_riscv_pte_paddr_aligned(self.0); + assert(PAGE_SIZE == 4096usize) by (compute_only); + assert(self.paddr() % PAGE_SIZE == 0); + } +} + +#[verifier::bit_vector] +proof fn lemma_riscv_pte_paddr_aligned(raw: usize) + ensures + RiscvPteModel::paddr_from_raw_spec(raw) % 4096usize == 0, +{ } +} // verus! impl fmt::Debug for PageTableEntry { fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { let mut f = f.debug_struct("PageTableEntry"); @@ -222,6 +1400,7 @@ impl fmt::Debug for PageTableEntry { } } +#[cfg(target_arch = "riscv64")] pub(crate) fn __memcpy_fallible(dst: *mut u8, src: *const u8, size: usize) -> usize { // TODO: implement fallible unsafe { @@ -231,6 +1410,7 @@ pub(crate) fn __memcpy_fallible(dst: *mut u8, src: *const u8, size: usize) -> us 0 } +#[cfg(target_arch = "riscv64")] pub(crate) fn __memset_fallible(dst: *mut u8, value: u8, size: usize) -> usize { // TODO: implement fallible unsafe { diff --git a/ostd/src/arch/x86/mm/mod.rs b/ostd/src/arch/x86/mm/mod.rs index 4a2bc573d..cf5b427d3 100644 --- a/ostd/src/arch/x86/mm/mod.rs +++ b/ostd/src/arch/x86/mm/mod.rs @@ -20,7 +20,7 @@ use crate::{ mm::{ page_prop::{CachePolicy, PageFlags, PageProperty, PrivilegedPageFlags as PrivFlags}, page_table::{PageTableEntryTrait, PageTableFrag}, - Paddr, PagingConstsTrait, PagingLevel, PodOnce, Vaddr, + CurrentPagingConstsTrait, Paddr, PagingConstsTrait, PagingLevel, PodOnce, Vaddr, }, Pod, }; @@ -116,6 +116,15 @@ impl PagingConstsTrait for PagingConsts { } } +impl CurrentPagingConstsTrait for PagingConsts { + proof fn lemma_current_paging_consts_requirements() { + Self::lemma_paging_consts_requirements(); + assert(Self::BASE_PAGE_SIZE() == PAGE_SIZE) by (compute_only); + assert(Self::NR_LEVELS() == NR_LEVELS as PagingLevel) by (compute_only); + assert(Self::BASE_PAGE_SIZE() / Self::PTE_SIZE() == NR_ENTRIES) by (compute_only); + } +} + pub proof fn lemma_nr_subpage_per_huge_eq_nr_entries() ensures crate::mm::nr_subpage_per_huge::() == NR_ENTRIES, @@ -392,7 +401,6 @@ impl PageTableEntryTrait for PageTableEntry { fn paddr(&self) -> Paddr { proof { self.lemma_paddr_is_page_aligned(); - assume(self.0 & Self::PHYS_ADDR_MASK < MAX_PADDR); } self.0 & Self::PHYS_ADDR_MASK } diff --git a/ostd/src/mm/kspace/mod.rs b/ostd/src/mm/kspace/mod.rs index 4ecb4cfd4..bb4413f05 100644 --- a/ostd/src/mm/kspace/mod.rs +++ b/ostd/src/mm/kspace/mod.rs @@ -44,7 +44,7 @@ pub(crate) mod kvirt_area; mod test; use super::{ - Paddr, PagingConstsTrait, Vaddr, + CurrentPagingConstsTrait, Paddr, PagingConstsTrait, Vaddr, frame::{ Frame, Segment, meta::{AnyFrameMeta, MetaPageMeta, MetaSlot, mapping}, @@ -177,6 +177,7 @@ unsafe impl PageTableConfig for KernelPtConfig { use crate::mm::nr_subpage_per_huge; use vstd::arithmetic::power2::{lemma2_to64, lemma2_to64_rest, lemma_pow2_adds, pow2}; Self::C::lemma_paging_consts_properties(); + Self::C::lemma_current_paging_consts_requirements(); PageTableEntry::lemma_layout(); lemma2_to64(); lemma2_to64_rest(); diff --git a/ostd/src/mm/mod.rs b/ostd/src/mm/mod.rs index 218886da8..d3d2ea5c4 100644 --- a/ostd/src/mm/mod.rs +++ b/ostd/src/mm/mod.rs @@ -125,17 +125,6 @@ pub trait PagingConstsTrait: Clone + Debug + Send + Sync + 'static { /// NOTE: The postcondition is designed to be minimal, to actually be used in proofs, call `lemma_paging_consts_properties` /// instead to get all the properties that are derived from the requirements. /// - /// FIXME： General architecture support. - /// All configs in vostd use the same value for the per-config - /// `NR_LEVELS()` as the architecture-level constant `NR_LEVELS` - /// (= 4 for x86_64). This is *implicit* in the cursor framework: - /// `CursorOwner::inv()` hardcodes `self.level <= NR_LEVELS` (const) - /// for cursors over any `C: PagingConstsTrait`, so a config whose - /// `NR_LEVELS_spec()` exceeded `NR_LEVELS` would be unusable. This - /// lemma exposes that equality as a usable fact so generic proofs - /// can chain `level != C::NR_LEVELS_spec()` to `level < NR_LEVELS` - /// (e.g. `Cursor::find_next_impl`'s PageTable-branch gate ⟹ - /// `CursorMut::take_next`'s `replace_cur_entry` discharge). proof fn lemma_paging_consts_requirements() ensures 0 < Self::BASE_PAGE_SIZE(), @@ -147,12 +136,6 @@ pub trait PagingConstsTrait: Clone + Debug + Send + Sync + 'static { Self::BASE_PAGE_SIZE().ilog2() + (Self::BASE_PAGE_SIZE() / Self::PTE_SIZE()).ilog2() * Self::NR_LEVELS() <= Self::ADDRESS_WIDTH(), Self::PTE_SIZE() == core::mem::size_of::(), - // The following statement holds for all architectures, - // but the actual value of the constants may vary. - // Maybe we can remove this requirement. - Self::BASE_PAGE_SIZE() == PAGE_SIZE, - Self::NR_LEVELS() == NR_LEVELS, - Self::BASE_PAGE_SIZE() / Self::PTE_SIZE() == NR_ENTRIES, ; /// The derived properties of the paging constants. @@ -165,7 +148,6 @@ pub trait PagingConstsTrait: Clone + Debug + Send + Sync + 'static { Self::BASE_PAGE_SIZE().ilog2() + (Self::BASE_PAGE_SIZE() / Self::PTE_SIZE()).ilog2() * ( Self::NR_LEVELS() - 1) <= Self::ADDRESS_WIDTH(), 0 < Self::BASE_PAGE_SIZE() / Self::PTE_SIZE() <= Self::BASE_PAGE_SIZE(), - NR_ENTRIES * Self::PTE_SIZE() == PAGE_SIZE, // Copied from the postcondition of `lemma_paging_consts_requirements` // so that we only need to call this lemma in proofs. 0 < Self::BASE_PAGE_SIZE(), @@ -177,25 +159,57 @@ pub trait PagingConstsTrait: Clone + Debug + Send + Sync + 'static { Self::BASE_PAGE_SIZE().ilog2() + (Self::BASE_PAGE_SIZE() / Self::PTE_SIZE()).ilog2() * Self::NR_LEVELS() <= Self::ADDRESS_WIDTH(), Self::PTE_SIZE() == core::mem::size_of::(), - // The following statement holds for all architectures, - // but the actual value of the constants may vary. - // Maybe we can remove this requirement. - Self::BASE_PAGE_SIZE() == PAGE_SIZE, - Self::NR_LEVELS() == NR_LEVELS, - Self::BASE_PAGE_SIZE() / Self::PTE_SIZE() == NR_ENTRIES, { Self::lemma_paging_consts_requirements(); broadcast use group_div_basics; + let base = Self::BASE_PAGE_SIZE() as int; + let pte = Self::PTE_SIZE() as int; + let levels = Self::NR_LEVELS() as int; + let base_bits = Self::BASE_PAGE_SIZE().ilog2() as int; + let index_bits = (Self::BASE_PAGE_SIZE() / Self::PTE_SIZE()).ilog2() as int; + assert(0 < base / pte) by { + vstd::arithmetic::div_mod::lemma_div_non_zero(base, pte); + }; + assert(base / pte <= base) by { + vstd::arithmetic::div_mod::lemma_div_is_ordered(0, base, pte); + }; + assert(base_bits + index_bits * (levels - 1) <= base_bits + index_bits * levels) + by (nonlinear_arith) + requires + 0 <= index_bits, + 1 <= levels, + ; } } -pub open spec fn page_size_spec(level: PagingLevel) -> usize { - (PAGE_SIZE * pow2( - (nr_subpage_per_huge::().ilog2() * (level - 1)) as nat, +/// Compatibility facts for proof modules that still use the current target's +/// fixed page-table node geometry. +/// +/// This is intentionally separate from [`PagingConstsTrait`]. A future +/// architecture may implement the generic paging contract without claiming +/// the x86 verification target's 4 KiB/4-level/512-entry layout. +pub trait CurrentPagingConstsTrait: PagingConstsTrait { + proof fn lemma_current_paging_consts_requirements() + ensures + Self::BASE_PAGE_SIZE() == PAGE_SIZE, + Self::NR_LEVELS() == NR_LEVELS as PagingLevel, + Self::BASE_PAGE_SIZE() / Self::PTE_SIZE() == NR_ENTRIES, + ; +} + +/// The page-size formula for an explicit paging configuration. +pub open spec fn page_size_for_spec(level: PagingLevel) -> usize { + (C::BASE_PAGE_SIZE_spec() * pow2( + (nr_subpage_per_huge::().ilog2() * (level - 1)) as nat, )) as usize } +/// The page-size formula for the architecture selected by this build. +pub open spec fn page_size_spec(level: PagingLevel) -> usize { + page_size_for_spec::(level) +} + // /// The page size // pub const PAGE_SIZE: usize = page_size::(1); /// The page size at a given level. @@ -233,7 +247,7 @@ pub fn page_size(level: PagingLevel) -> (ret: usize) #[verifier::inline] pub open spec fn nr_subpage_per_huge_spec() -> usize { - C::BASE_PAGE_SIZE() / C::PTE_SIZE() + C::BASE_PAGE_SIZE_spec() / C::PTE_SIZE_spec() } /// The number of sub pages in a huge page. diff --git a/ostd/src/mm/page_table/cursor/mod.rs b/ostd/src/mm/page_table/cursor/mod.rs index 7464713b0..5b6f348da 100644 --- a/ostd/src/mm/page_table/cursor/mod.rs +++ b/ostd/src/mm/page_table/cursor/mod.rs @@ -63,8 +63,9 @@ use crate::{ }; use super::{ - Child, ChildRef, Entry, EntryOwner, FrameView, PageTable, PageTableConfig, PageTableError, - PageTableGuard, PageTablePageMeta, PagingConstsTrait, PagingLevel, pte_index, + Child, ChildRef, CurrentPagingConstsTrait, Entry, EntryOwner, FrameView, PageTable, + PageTableConfig, PageTableError, PageTableGuard, PageTablePageMeta, PagingConstsTrait, + PagingLevel, pte_index, }; verus! { @@ -1093,6 +1094,7 @@ impl<'rcu, C: PageTableConfig, A: InAtomicMode> Cursor<'rcu, C, A> { } if !C::TOP_LEVEL_CAN_UNMAP_spec() { C::lemma_paging_consts_properties(); + C::lemma_current_paging_consts_requirements(); assert(self.level < NR_LEVELS); } } diff --git a/ostd/src/mm/page_table/mod.rs b/ostd/src/mm/page_table/mod.rs index bbb11f2ca..49aabad33 100644 --- a/ostd/src/mm/page_table/mod.rs +++ b/ostd/src/mm/page_table/mod.rs @@ -29,7 +29,7 @@ use core::{ }; use super::{ - Paddr, PagingConstsTrait, PagingLevel, PodOnce, Vaddr, + CurrentPagingConstsTrait, Paddr, PagingConstsTrait, PagingLevel, PodOnce, Vaddr, kspace::KernelPtConfig, nr_subpage_per_huge, page_prop::{CachePolicy, PageProperty}, @@ -181,7 +181,7 @@ pub unsafe trait PageTableConfig: Clone + Debug + Send + Sync + 'static { type E: PageTableEntryTrait; /// The paging constants. - type C: PagingConstsTrait; + type C: CurrentPagingConstsTrait; /// The item that can be mapped into the virtual memory space using the /// page table. @@ -499,6 +499,7 @@ pub unsafe trait PageTableConfig: Clone + Debug + Send + Sync + 'static { ) == NR_ENTRIES, { Self::C::lemma_paging_consts_properties(); + Self::C::lemma_current_paging_consts_requirements(); Self::lemma_page_table_config_constant_requirements(); } } @@ -562,6 +563,12 @@ impl PagingConstsTrait for C { } } +impl CurrentPagingConstsTrait for C { + proof fn lemma_current_paging_consts_requirements() { + C::C::lemma_current_paging_consts_requirements(); + } +} + /// Splits the address range into largest page table items. /// /// Each of the returned items is a tuple of the physical address and the @@ -626,6 +633,7 @@ fn top_level_index_width() -> (ret: usize) { proof { C::lemma_paging_consts_properties(); + C::lemma_current_paging_consts_requirements(); C::lemma_page_table_config_constant_properties(); } @@ -640,6 +648,7 @@ fn pt_va_range_start() -> (ret: Vaddr) { proof { C::lemma_paging_consts_properties(); + C::lemma_current_paging_consts_requirements(); let ghost idx_start = C::TOP_LEVEL_INDEX_RANGE().start; let ghost offset = pte_index_bit_offset_spec::(C::NR_LEVELS()); crate::specs::mm::page_table::vaddr_range_proofs::lemma_pt_va_range_start_shift_facts::( @@ -666,6 +675,7 @@ fn pt_va_range_end() -> (ret: Vaddr) let idx_end = C::TOP_LEVEL_INDEX_RANGE().end; proof { C::lemma_paging_consts_properties(); + C::lemma_current_paging_consts_requirements(); } let offset = pte_index_bit_offset::(C::NR_LEVELS()); @@ -818,7 +828,7 @@ fn nr_pte_index_bits() -> usize } /// The index of a VA's PTE in a page table node at the given level. -fn pte_index(va: Vaddr, level: PagingLevel) -> (res: usize) +fn pte_index(va: Vaddr, level: PagingLevel) -> (res: usize) requires 1 <= level <= NR_LEVELS, ensures @@ -827,6 +837,7 @@ fn pte_index(va: Vaddr, level: PagingLevel) -> (res: usize proof { let offset = pte_index_bit_offset_spec::(level); C::lemma_paging_consts_properties(); + C::lemma_current_paging_consts_requirements(); lemma_arch_specific_consts_properties::(); assert(0 <= offset < usize::BITS) by (nonlinear_arith) requires @@ -850,7 +861,7 @@ fn pte_index(va: Vaddr, level: PagingLevel) -> (res: usize /// This function returns the bit offset of the least significant bit. Take /// x86-64 as an example, the `pte_index_bit_offset(2)` should return 21, which /// is 12 (the 4KiB in-page offset) plus 9 (index width in the level-1 table). -fn pte_index_bit_offset(level: PagingLevel) -> usize +fn pte_index_bit_offset(level: PagingLevel) -> usize requires 1 <= level <= NR_LEVELS, returns @@ -858,6 +869,7 @@ fn pte_index_bit_offset(level: PagingLevel) -> usize { proof { C::lemma_paging_consts_properties(); + C::lemma_current_paging_consts_requirements(); lemma_arch_specific_consts_properties::(); assert(12 + 9 * (level - 1) <= 39) by (nonlinear_arith) requires @@ -1678,7 +1690,7 @@ pub trait PageTableEntryTrait: #[verifier::when_used_as_spec(paddr_spec)] fn paddr(&self) -> (res: Paddr) ensures - valid_frame_paddr(res), + res % PAGE_SIZE == 0, returns self.paddr(), ; diff --git a/ostd/src/mm/page_table/node/mod.rs b/ostd/src/mm/page_table/node/mod.rs index 46be42ec7..35c8bf613 100644 --- a/ostd/src/mm/page_table/node/mod.rs +++ b/ostd/src/mm/page_table/node/mod.rs @@ -72,6 +72,7 @@ use super::{PageTableConfig, PageTableEntryTrait, nr_subpage_per_huge}; use crate::{ mm::{ + CurrentPagingConstsTrait, PagingConstsTrait, PagingLevel, // FrameAllocOptions, Infallible, @@ -174,6 +175,7 @@ unsafe impl AnyFrameMeta for PageTablePageMeta { proof { C::lemma_paging_consts_properties(); + C::lemma_current_paging_consts_requirements(); C::lemma_page_table_config_constant_properties(); vstd::arithmetic::mul::lemma_mul_inequality( range.start as int, @@ -217,6 +219,7 @@ unsafe impl AnyFrameMeta for PageTablePageMeta { proof { C::lemma_page_table_config_constant_properties(); C::lemma_paging_consts_properties(); + C::lemma_current_paging_consts_requirements(); vstd::arithmetic::mul::lemma_mul_is_distributive_sub_other_way( size_of_e, NR_ENTRIES as int, @@ -1002,11 +1005,10 @@ impl PageTablePageMeta { ensures ({ let pte = Self::walk_pte_at_view(view, c); - pte.is_present() && pte.is_last(self.level) ==> C::raw_item_well_formed( - pte.paddr(), - self.level, - pte.prop(), - ) + pte.is_present() && pte.is_last(self.level) ==> { + &&& valid_frame_paddr(pte.paddr()) + &&& C::raw_item_well_formed(pte.paddr(), self.level, pte.prop()) + } }), { } @@ -1061,8 +1063,8 @@ impl PageTablePageMeta { } } - /// Every present leaf PTE encountered by the drop walk contains a canonical - /// raw item for the node's paging level. + /// Every present leaf PTE encountered by the drop walk contains a valid + /// frame address and a canonical raw item for the node's paging level. pub open spec fn walk_items_well_formed_from_view( self, reader: crate::mm::VmReader<'_, crate::mm::Infallible>, @@ -1075,11 +1077,10 @@ impl PageTablePageMeta { C::E, >() as int == 0 ==> { let pte = Self::walk_pte_at_view(view, c); - pte.is_present() && pte.is_last(self.level) ==> C::raw_item_well_formed( - pte.paddr(), - self.level, - pte.prop(), - ) + pte.is_present() && pte.is_last(self.level) ==> { + &&& valid_frame_paddr(pte.paddr()) + &&& C::raw_item_well_formed(pte.paddr(), self.level, pte.prop()) + } } } diff --git a/ostd/src/mm/vm_space.rs b/ostd/src/mm/vm_space.rs index c4abdfe24..d1bcb6e9a 100644 --- a/ostd/src/mm/vm_space.rs +++ b/ostd/src/mm/vm_space.rs @@ -45,7 +45,7 @@ use crate::mm::tlb::*; use crate::specs::mm::cpu::{AtomicCpuSet, CpuSet}; use crate::mm::{ - MAX_USERSPACE_VADDR, Paddr, PagingConstsTrait, PagingLevel, Vaddr, + CurrentPagingConstsTrait, MAX_USERSPACE_VADDR, Paddr, PagingConstsTrait, PagingLevel, Vaddr, io::{Fallible, VmReader, VmWriter}, page_prop::PageProperty, }; @@ -1764,6 +1764,7 @@ unsafe impl PageTableConfig for UserPtConfig { lemma_pow2_adds(9, 39); PageTableEntry::lemma_layout(); Self::C::lemma_paging_consts_properties(); + Self::C::lemma_current_paging_consts_requirements(); assert(Self::LEADING_BITS_spec() == 0usize); } }