make read_val-* not trusted and move primitives for Pods as trusted wrappers (#345)

Author: hiroki-chen

ostd/specs/mm/page_table/node/child.rs

@@ -52,7 +52,7 @@ impl<'a, C: PageTableConfig> OwnerOf for ChildRef<'a, C> {
             Self::None => owner.is_absent(),
         }
     }
-}    
+}
 
 impl<C: PageTableConfig> Child<C> {
 

ostd/specs/mm/page_table/owners.rs

@@ -13,13 +13,10 @@ use vstd_extra::ghost_tree::*;
 use vstd_extra::ownership::*;
 use vstd_extra::prelude::TreeNodeValue;
 
-use crate::mm::{
-    page_table::EntryOwner,
-    Paddr, PagingLevel, Vaddr, MAX_NR_LEVELS,
-};
+use crate::mm::{page_table::EntryOwner, Paddr, PagingLevel, Vaddr, MAX_NR_LEVELS};
 
 use crate::mm::frame::frame_to_index;
-use crate::mm::page_table::{PageTableGuard, PageTableEntryTrait};
+use crate::mm::page_table::{PageTableEntryTrait, PageTableGuard};
 
 use crate::specs::arch::*;
 use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;

ostd/src/mm/frame/frame_ref.rs

@@ -67,6 +67,7 @@ impl<M: AnyFrameMeta> FrameRef<'_, M> {
     pub(in crate::mm) fn borrow_paddr(raw: Paddr) -> Self {
         proof {
             broadcast use crate::mm::frame::meta::mapping::group_page_meta;
+
             old(regions).inv_implies_correct_addr(raw);
         }
 

ostd/src/mm/frame/mod.rs

@@ -417,8 +417,8 @@ impl<'a, M: AnyFrameMeta> Frame<M> {
     pub fn borrow(&self) -> FrameRef<'a, M> {
         assert(regions.slot_owners.contains_key(self.index()));
         broadcast use crate::mm::frame::meta::mapping::group_page_meta;
-
         // SAFETY: Both the lifetime and the type matches `self`.
+
         #[verus_spec(with Tracked(&perm.points_to))]
         let paddr = self.start_paddr();