fix unverified code

ostd/src/arch/x86/mm/mod.rs

@@ -105,6 +105,9 @@ impl PagingConstsTrait for PagingConsts {
     proof fn lemma_paging_consts_properties()
     {
         lemma_pow2_is_pow2_to64();
+        assert(PAGE_SIZE == 4096usize);
+        assert(NR_ENTRIES == 512usize);
+        assert(Self::BASE_PAGE_SIZE_spec() / Self::PTE_SIZE_spec() == NR_ENTRIES);
     }
 }
 

ostd/src/mm/kspace/kvirt_area.rs

@@ -678,6 +678,8 @@ impl KVirtArea {
         };
         let preempt_guard = disable_preempt::<A>();
 
+        let ghost pre_cursor_regions: MetaRegionOwners = *regions;
+
         #[verus_spec(with Tracked(owner.pt_owner), Ghost(root_guard), Tracked(regions), Tracked(guards))]
         let cursor_res = page_table.cursor_mut(preempt_guard, &cursor_range);
 
@@ -707,6 +709,36 @@ impl KVirtArea {
         assert!(cursor_res.is_ok());
         let (mut cursor, Tracked(cursor_owner)) = cursor_res.unwrap();
 
+        proof {
+            assert(pre_cursor_regions == *old(regions));
+            assert forall|i: int| 0 <= i < frames.len() implies CursorMut::<
+                'a,
+                KernelPtConfig,
+                A,
+            >::item_slot_in_regions(MappedItem::Tracked(#[trigger] frames[i], prop), *regions) by {
+                let item_i = MappedItem::Tracked(frames[i], prop);
+                let pa_i = KernelPtConfig::item_into_raw_spec(item_i).0;
+                let idx_i = frame_to_index(pa_i);
+                KernelPtConfig::item_into_raw_spec_tracked_level(item_i);
+                assert(CursorMut::<'a, KernelPtConfig, A>::item_slot_in_regions(
+                    item_i,
+                    pre_cursor_regions,
+                ));
+                assert(pre_cursor_regions.slots.contains_key(idx_i));
+                assert(pre_cursor_regions.inv());
+                assert(pre_cursor_regions.slot_owners.contains_key(idx_i));
+                assert(pre_cursor_regions.slot_owners[idx_i].inner_perms.ref_count.value()
+                    != crate::specs::mm::frame::meta_owners::REF_COUNT_UNUSED);
+                assert(regions.slot_owners[idx_i].inner_perms.ref_count.value()
+                    == pre_cursor_regions.slot_owners[idx_i].inner_perms.ref_count.value());
+                assert(idx_i < crate::specs::mm::frame::mapping::max_meta_slots());
+                assert(regions.inv());
+                assert(regions.slot_owners.contains_key(idx_i));
+                assert(regions.slots.contains_key(idx_i));
+            };
+        }
+
+        let ghost mut mapped_pages: int = 0;
         for frame in it: frames.into_iter()
             invariant
                 cursor.0.invariants(cursor_owner, *regions, *guards),
@@ -722,11 +754,16 @@ impl KVirtArea {
                 // > area_size` derivation that fires `map_frames_bounds_panic_condition`'s
                 // capacity disjunct ⟹ `may_panic()` via the invariant.
                 it.seq().len() == frames.len(),
+                0 <= mapped_pages <= frames.len(),
+                mapped_pages == it.index(),
                 cursor.0.barrier_va.start == range.start + map_offset,
                 cursor.0.barrier_va.end == range.end,
                 cursor.0.guard_level == NR_LEVELS as u8,
+                cursor.0.va <= cursor.0.barrier_va.end,
                 range.end - range.start == area_size,
                 cursor.0.va == range.start + map_offset + it.index() * PAGE_SIZE,
+                cursor.0.va as int == range.start as int + map_offset as int + mapped_pages
+                    * PAGE_SIZE as int,
                 // For each remaining frame, the map contains a wf owner at its paddr.
                 // Duplicates among remaining frames are fine — one key, one owner.
                 forall|i: int|
@@ -991,10 +1028,24 @@ impl KVirtArea {
                 );
                 fresh.in_scope = false;
                 entry_owners.tracked_insert(cur_mapped_pa, fresh);
+                mapped_pages = mapped_pages + 1;
             }
         }
 
         proof {
+            assert(mapped_pages == frames.len());
+            assert(cursor.0.va as int == range.start as int + map_offset as int
+                + frames.len() as int * PAGE_SIZE as int);
+            assert(cursor.0.va <= cursor.0.barrier_va.end);
+            assert(map_offset as int + frames.len() as int * PAGE_SIZE as int <= area_size as int)
+                by (nonlinear_arith)
+                requires
+                    cursor.0.va as int == range.start as int + map_offset as int
+                        + frames.len() as int * PAGE_SIZE as int,
+                    cursor.0.va <= cursor.0.barrier_va.end,
+                    cursor.0.barrier_va.end == range.end,
+                    range.end - range.start == area_size,
+            ;
             // The diverging `assert!`s at the top (`area_size % PAGE_SIZE`
             // and `map_offset % PAGE_SIZE`) did not fire, so the
             // caller-precludable panic condition is false on this path.
@@ -1029,6 +1080,27 @@ impl KVirtArea {
         ||| kvirt_alloc_oom_condition(area_size)
     }
 
+    /// Metadata obligation for mapping untracked physical frames.
+    ///
+    /// `map_untracked_frames` is unsafe: the caller must ensure the physical
+    /// range is managed metadata-wise even though it does not carry `Frame`
+    /// ownership. The page-table cursor only needs page-sized slot facts for
+    /// the MMIO leaves it creates.
+    pub open spec fn untracked_range_slots_in_regions(
+        pa_range: &Range<Paddr>,
+        regions: MetaRegionOwners,
+    ) -> bool {
+        &&& pa_range.end <= MAX_PADDR
+        &&& forall|pa: Paddr|
+            #![trigger crate::mm::frame::meta::mapping::frame_to_index(pa)]
+            pa_range.start <= pa < pa_range.end && pa % PAGE_SIZE == 0 ==> {
+                let idx = crate::mm::frame::meta::mapping::frame_to_index(pa);
+                &&& regions.slots.contains_key(idx)
+                &&& regions.slot_owners[idx].inner_perms.ref_count.value()
+                    != crate::specs::mm::frame::meta_owners::REF_COUNT_UNUSED
+            }
+    }
+
     /// Creates a kernel virtual area and maps untracked frames into it.
     ///
     /// The created virtual area will have a size of `area_size`, and the
@@ -1068,6 +1140,7 @@ impl KVirtArea {
             kvirt_alloc_oom_condition(area_size) ==> may_panic(),
             old(regions).inv(),
             owner.inv(),
+            Self::untracked_range_slots_in_regions(&pa_range, *old(regions)),
             map_offset + vstd_extra::external::range::range_usize_len(&pa_range) <= usize::MAX,
         ensures
             final(regions).inv(),
@@ -1136,6 +1209,33 @@ impl KVirtArea {
 
             let (mut cursor, Tracked(cursor_owner)) = cursor_res.unwrap();
 
+            proof {
+                assert(pre_cursor_regions == *old(regions));
+                assert(Self::untracked_range_slots_in_regions(&pa_range, pre_cursor_regions));
+                assert(pa_range.end <= MAX_PADDR);
+                assert forall|pa: Paddr|
+                    #![trigger crate::mm::frame::meta::mapping::frame_to_index(pa)]
+                    pa_range.start <= pa < pa_range.end && pa % PAGE_SIZE == 0 implies {
+                    let idx = crate::mm::frame::meta::mapping::frame_to_index(pa);
+                    &&& regions.slots.contains_key(idx)
+                    &&& regions.slot_owners[idx].inner_perms.ref_count.value()
+                        != crate::specs::mm::frame::meta_owners::REF_COUNT_UNUSED
+                } by {
+                    let idx = crate::mm::frame::meta::mapping::frame_to_index(pa);
+                    assert(pre_cursor_regions.slots.contains_key(idx));
+                    assert(pre_cursor_regions.inv());
+                    assert(pre_cursor_regions.slot_owners.contains_key(idx));
+                    assert(pre_cursor_regions.slot_owners[idx].inner_perms.ref_count.value()
+                        != crate::specs::mm::frame::meta_owners::REF_COUNT_UNUSED);
+                    assert(regions.slot_owners[idx].inner_perms.ref_count.value()
+                        == pre_cursor_regions.slot_owners[idx].inner_perms.ref_count.value());
+                    assert(idx < crate::specs::mm::frame::mapping::max_meta_slots());
+                    assert(regions.inv());
+                    assert(regions.slot_owners.contains_key(idx));
+                    assert(regions.slots.contains_key(idx));
+                };
+            }
+
             let pages = collect_largest_pages(va_range.start, pa_range.start, len);
 
             for (pa, level) in it: pages.into_iter()

ostd/src/mm/kspace/mod.rs

@@ -216,6 +216,15 @@ unsafe impl PageTableConfig for KernelPtConfig {
         assert((((Self::TOP_LEVEL_INDEX_RANGE_spec().start as int) * (pow2(
             pte_index_bit_offset_spec::<Self::C>(Self::C::NR_LEVELS()) as nat,
         ) as int)) / (pow2((Self::C::ADDRESS_WIDTH() - 1) as nat) as int)) % 2 == 1);
+        lemma_pow2_adds(16, 48);
+        assert(Self::LEADING_BITS_spec() == 0xffffusize);
+        assert(pow2(48) == 0x1_0000_0000_0000nat);
+        assert(pow2(64) == 0x1_0000_0000_0000_0000nat);
+        assert((0xffffint + 1int) * 0x1_0000_0000_0000int == 0x1_0000_0000_0000_0000int);
+        assert(0xffffint * 0x1_0000_0000_0000int == 0x1_0000_0000_0000_0000int
+            - 0x1_0000_0000_0000int);
+        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);
     }
 
     fn TOP_LEVEL_INDEX_RANGE() -> (r: Range<usize>)

ostd/src/mm/mod.rs

@@ -142,10 +142,12 @@ pub trait PagingConstsTrait: Clone + Debug + Send + Sync + 'static {
         ensures
             0 < Self::BASE_PAGE_SIZE_spec(),
             is_pow2(Self::BASE_PAGE_SIZE_spec() as int),
+            Self::BASE_PAGE_SIZE_spec() == PAGE_SIZE,
             Self::NR_LEVELS_spec() > 0,
             Self::NR_LEVELS_spec() == NR_LEVELS,
             is_pow2(Self::PTE_SIZE_spec() as int),
             0 < Self::PTE_SIZE_spec() <= Self::BASE_PAGE_SIZE_spec(),
+            Self::BASE_PAGE_SIZE_spec() / Self::PTE_SIZE_spec() == NR_ENTRIES,
     ;
 }
 

ostd/src/mm/page_table/cursor/locking.rs

@@ -45,6 +45,7 @@ pub assume_specification<Idx: Clone>[ Range::<Idx>::clone ](range: &Range<Idx>)
         ret.0.invariants(*ret.1, *final(regions), *final(guards)),
         (*ret.1).in_locked_range(),
         ret.0.level == ret.0.guard_level,
+        ret.0.guard_level == NR_LEVELS as PagingLevel,
         ret.0.va < ret.0.barrier_va.end,
         ret.0.va == va.start,
         ret.0.barrier_va == *va,

ostd/src/mm/page_table/cursor/mod.rs

@@ -301,6 +301,7 @@ impl<'rcu, C: PageTableConfig, A: InAtomicMode> Cursor<'rcu, C, A> {
                 &&& r.unwrap().0.invariants(*r.unwrap().1, *final(regions), *final(guards))
                 &&& r.unwrap().1.in_locked_range()
                 &&& r.unwrap().0.level == r.unwrap().0.guard_level
+                &&& r.unwrap().0.guard_level == NR_LEVELS as PagingLevel
                 &&& r.unwrap().0.va < r.unwrap().0.barrier_va.end
                 &&& r.unwrap().0.va == va.start
                 &&& r.unwrap().0.barrier_va == *va
@@ -2087,6 +2088,7 @@ impl<'rcu, C: PageTableConfig, A: InAtomicMode> CursorMut<'rcu, C, A> {
                 &&& r.unwrap().0.0.invariants(*r.unwrap().1, *final(regions), *final(guards))
                 &&& r.unwrap().1.in_locked_range()
                 &&& r.unwrap().0.0.level == r.unwrap().0.0.guard_level
+                &&& r.unwrap().0.0.guard_level == NR_LEVELS as PagingLevel
                 &&& r.unwrap().0.0.va < r.unwrap().0.0.barrier_va.end
                 &&& r.unwrap().0.0.va == va.start
                 &&& r.unwrap().0.0.barrier_va == *va
@@ -2106,6 +2108,14 @@ impl<'rcu, C: PageTableConfig, A: InAtomicMode> CursorMut<'rcu, C, A> {
                     != crate::specs::mm::frame::meta_owners::REF_COUNT_UNUSED
                 ==> final(regions).slot_owners[idx].paths_in_pt
                         == old(regions).slot_owners[idx].paths_in_pt,
+            forall|idx: usize| #![trigger final(regions).slot_owners[idx]]
+                old(regions).slot_owners.contains_key(idx)
+                && old(regions).slot_owners[idx].inner_perms.ref_count.value()
+                    != crate::specs::mm::frame::meta_owners::REF_COUNT_UNUSED
+                ==> final(regions).slot_owners[idx].inner_perms.ref_count.value()
+                        == old(regions).slot_owners[idx].inner_perms.ref_count.value()
+                    && final(regions).slot_owners[idx].usage
+                        == old(regions).slot_owners[idx].usage,
     )]
     pub fn new(pt: &'rcu PageTable<C>, guard: &'rcu A, va: &Range<Vaddr>) -> Result<
         (Self, Tracked<CursorOwner<'rcu, C>>),