Merge remote-tracking branch 'origin/main' into paging-const

Resolved conflicts between paging-const genericization and upstream
changes (PRs asterinas#531, asterinas#534, asterinas#537). Adapted upstream's new proven proofs
to use generic C::NR_LEVELS()/nr_subpage_per_huge::<C>() forms.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: Marsman1996

ostd/specs/mm/page_table/cursor/cursor_fn_lemmas.rs

@@ -17,6 +17,7 @@ use vstd_extra::arithmetic::{
     lemma_nat_align_up_sound,
 };
 
+use crate::arch::mm::PagingConsts;
 use crate::mm::nr_subpage_per_huge;
 use crate::mm::page_table::*;
 use crate::mm::{PagingConstsTrait, PagingLevel, Vaddr, page_size};
@@ -334,7 +335,93 @@ impl<'rcu, C: PageTableConfig> CursorOwner<'rcu, C> {
             self.continuations[j].path().index(self.continuations[i].path().len() as int)
                 == self.continuations[i].idx,
     {
-        admit();
+        C::lemma_paging_consts_properties();
+        assert(nr_subpage_per_huge::<C>() == NR_ENTRIES);
+        // Explicitly instantiate continuation invariants for all indices
+        // that the case branches use. inv_continuation(k) requires
+        // self.level - 1 <= k <= C::NR_LEVELS() - 1, which holds for
+        // all k in [j, i] since self.level - 1 <= j < i < C::NR_LEVELS().
+        self.inv_continuation(i);
+        self.inv_continuation(j);
+        // Also instantiate for intermediate indices used in the i==3,j==0
+        // and i==2,j==0 branches (they access continuations[1] and [2]).
+        if j < i - 1 {
+            // There's at least one index between j and i
+            self.inv_continuation(j + 1);
+            if j + 2 < i {
+                self.inv_continuation(j + 2);
+            }
+        }
+        if i == 3 && j == 2 {
+            self.continuations[3].path().push_tail_property_index(
+                self.continuations[3].idx as usize,
+            );
+            self.continuations[3].path().push_tail_property_len(self.continuations[3].idx as usize);
+        } else if i == 3 && j == 1 {
+            let p3 = self.continuations[3].path();
+            let p2 = self.continuations[2].path();
+            let idx3 = self.continuations[3].idx as usize;
+            let idx2 = self.continuations[2].idx as usize;
+            p3.push_tail_property_index(idx3);
+            p3.push_tail_property_len(idx3);
+            p2.push_tail_property_index(idx2);
+            p2.push_tail_property_len(idx2);
+            assert(p3.len() < p2.len());
+            assert(self.continuations[1].path() == p2.push_tail(idx2));
+            assert(p2.push_tail(idx2).index(p3.len() as int) == p2.index(p3.len() as int));
+        } else if i == 3 && j == 0 {
+            let p3 = self.continuations[3].path();
+            let p2 = self.continuations[2].path();
+            let p1 = self.continuations[1].path();
+            let idx3 = self.continuations[3].idx as usize;
+            let idx2 = self.continuations[2].idx as usize;
+            let idx1 = self.continuations[1].idx as usize;
+            p3.push_tail_property_index(idx3);
+            p3.push_tail_property_len(idx3);
+            p2.push_tail_property_index(idx2);
+            p2.push_tail_property_len(idx2);
+            p1.push_tail_property_index(idx1);
+            p1.push_tail_property_len(idx1);
+            assert(p3.len() < p2.len());
+            assert(p3.len() < p1.len());
+            assert(p1.push_tail(idx1).index(p3.len() as int) == p1.index(p3.len() as int));
+            assert(p2.push_tail(idx2).index(p3.len() as int) == p2.index(p3.len() as int));
+        } else if i == 2 && j == 1 {
+            self.continuations[2].path().push_tail_property_index(
+                self.continuations[2].idx as usize,
+            );
+            self.continuations[2].path().push_tail_property_len(self.continuations[2].idx as usize);
+        } else if i == 2 && j == 0 {
+            let p2 = self.continuations[2].path();
+            let p1 = self.continuations[1].path();
+            let idx2 = self.continuations[2].idx as usize;
+            let idx1 = self.continuations[1].idx as usize;
+            p2.push_tail_property_index(idx2);
+            p2.push_tail_property_len(idx2);
+            p1.push_tail_property_index(idx1);
+            p1.push_tail_property_len(idx1);
+            assert(p2.len() < p1.len());
+            assert(self.continuations[0].path() == p1.push_tail(idx1));
+            assert(p1.push_tail(idx1).index(p2.len() as int) == p1.index(p2.len() as int));
+            assert(p1 == p2.push_tail(idx2));
+            assert(p2.push_tail(idx2).index(p2.len() as int) == idx2);
+        } else if i == 1 && j == 0 {
+            self.continuations[1].path().push_tail_property_index(
+                self.continuations[1].idx as usize,
+            );
+            self.continuations[1].path().push_tail_property_len(self.continuations[1].idx as usize);
+        }
+    }
+
+    pub proof fn lemma_page_size_spec_5_eq_pow2_48()
+        ensures
+            page_size::<PagingConsts>(5) == pow2(48nat) as usize,
+    {
+        crate::arch::mm::lemma_nr_subpage_per_huge_eq_nr_entries();
+        vstd_extra::external::ilog2::lemma_usize_ilog2_to32();
+        vstd::arithmetic::power2::lemma2_to64();
+        vstd::arithmetic::power2::lemma2_to64_rest();
+        vstd::arithmetic::power2::lemma_pow2_adds(12nat, 36nat);
     }
 
     pub proof fn jump_not_in_node_level_lt_guard_minus_one(

ostd/specs/mm/page_table/cursor/cursor_steps.rs

@@ -1558,6 +1558,9 @@ impl<'rcu, C: PageTableConfig> CursorOwner<'rcu, C> {
             self.pop_level_owner().0.only_current_locked(guards),
             self.pop_level_owner().0.nodes_locked(guards),
             self.pop_level_owner().0.metaregion_sound(regions),
+            self.pop_level_owner().0.cur_entry_owner().is_node(),
+            self.pop_level_owner().1.inner.inner@.ptr.addr()
+                == self.pop_level_owner().0.cur_entry_owner().node().meta_addr_self(),
     {
         assume(nr_subpage_per_huge::<C>() == NR_ENTRIES);
         self.inv_continuation(self.level - 1);
@@ -1648,6 +1651,29 @@ impl<'rcu, C: PageTableConfig> CursorOwner<'rcu, C> {
                 }
             };
         };
+
+        // The cur_entry_owner of the popped owner is the child entry we just
+        // restored: new_cont.children[new_cont.idx] == Some(child_node)
+        // where child_node.value == child.entry_own, which is a node
+        // (from child.inv() => child.entry_own.is_node()).
+        assert(child.inv());
+        assert(child.entry_own.is_node());
+        assert(new_cont.idx == cont.idx);
+        assert(new_cont.children[new_cont.idx as int] == Some(child_node));
+        assert(child_node.value == child.entry_own);
+        // new_owner.level == self.level + 1
+        // new_owner.continuations[new_owner.level - 1] == new_cont
+        assert(new_owner.level == (self.level + 1) as u8);
+        assert(new_owner.continuations[new_owner.level as int - 1] == new_cont);
+        assert(new_owner.cur_entry_owner() == child.entry_own);
+        assert(new_owner.cur_entry_owner().is_node());
+        // The guard returned by pop_level_owner is child.guard (from restore).
+        // child.inv() gives relate_guard, so guard.addr == cur_entry_owner().node().meta_addr_self().
+        let (_new_owner, pop_guard) = self.pop_level_owner();
+        assert(pop_guard == child.guard);
+        assert(child.entry_own.node().relate_guard(child.guard));
+        assert(pop_guard.inner.inner@.ptr.addr()
+            == new_owner.cur_entry_owner().node().meta_addr_self());
     }
 
     /// Update va to a new value that shares the same indices at levels >= self.level.

ostd/specs/mm/page_table/cursor/owners.rs

@@ -941,6 +941,8 @@ impl<'rcu, C: PageTableConfig> CursorOwner<'rcu, C> {
         C::lemma_nr_subpage_per_huge_eq_nr_entries();
         assume(C::BASE_PAGE_SIZE() == PAGE_SIZE);
         C::lemma_paging_consts_requirements();
+        C::lemma_paging_consts_properties();
+        assert(nr_subpage_per_huge::<C>() == NR_ENTRIES);
         self.popped_too_high = false;
         let tracked mut cont = self.continuations.tracked_remove(self.level - 1);
         cont.do_inc_index();
@@ -2069,6 +2071,7 @@ impl<'rcu, C: PageTableConfig> CursorOwner<'rcu, C> {
         let big = 0x1_0000_0000_0000int;  // 2^48 == page_size(NR_LEVELS+1)
         let ps_nr = page_size::<C>(C::NR_LEVELS() as PagingLevel) as int;
 
+        crate::specs::arch::lemma_page_size_spec_values();
         // node_size == page_size_spec(5) == 2^48; page_size(NR_LEVELS) == 2^39 < 2^48.
 
         // ---- prefix.to_vaddr() == lb * 2^48 -------------------------------

ostd/specs/mm/page_table/cursor/page_size_lemmas.rs

@@ -2,12 +2,14 @@ use vstd::arithmetic::power2::pow2;
 use vstd::prelude::*;
 
 use crate::arch::mm::PagingConsts;
-use crate::mm::{Paddr, Vaddr, nr_subpage_per_huge, page_size};
-use crate::mm::{PagingConstsTrait, PagingLevel};
-use crate::specs::arch::*;
+use crate::mm::PagingLevel;
+use crate::mm::{KERNEL_VADDR_RANGE, MAX_PADDR, Paddr, Vaddr, nr_subpage_per_huge, page_size};
+use crate::mm::PagingConstsTrait;
+use crate::specs::arch::{NR_LEVELS, PAGE_SIZE};
 
 verus! {
 
+// ─── page_size(1) ──────────────────────────────────────────────────────
 /// page_size::<C>(1) == C::BASE_PAGE_SIZE.
 pub proof fn lemma_page_size_spec_level1<C: PagingConstsTrait>()
     ensures
@@ -22,8 +24,9 @@ pub proof fn lemma_page_size_spec_level1<C: PagingConstsTrait>()
     assume(PAGE_SIZE == C::BASE_PAGE_SIZE());
 }
 
-/// When `va` is aligned to `page_size::<C>(large_level)` and `level <= large_level`,
-/// then `va` is aligned to page_size::<C>(level).
+// ─── VA alignment ────────────────────────────────────────────────────────────
+/// When `va` is aligned to `page_size::<C>(large_level)` and `level <= large_level` (so
+/// page_size::<C>(level) divides page_size::<C>(large_level)), then `va` is aligned to page_size::<C>(level).
 pub proof fn lemma_va_align_page_size<C: PagingConstsTrait>(va: Vaddr, level: PagingLevel)
     requires
         1 <= level <= C::NR_LEVELS() + 1,
@@ -63,6 +66,8 @@ pub proof fn lemma_va_align_page_size<C: PagingConstsTrait>(va: Vaddr, level: Pa
     }
 }
 
+/// Special case for level 1: page_size::<C>(1) == C::BASE_PAGE_SIZE(), so va % C::BASE_PAGE_SIZE() == 0 implies
+/// va % page_size::<C>(1) == 0.
 pub proof fn lemma_va_align_page_size_level_1<C: PagingConstsTrait>(va: Vaddr)
     requires
         va % C::BASE_PAGE_SIZE() == 0,

ostd/specs/mm/page_table/mod.rs

@@ -22,6 +22,7 @@ use core::marker::PhantomData;
 
 use crate::mm::page_table::PageTableConfig;
 use crate::mm::{PagingConstsTrait, PagingLevel, Vaddr, nr_subpage_per_huge, page_size};
+use crate::arch::mm::PagingConsts;
 use crate::specs::arch::*;
 
 use align_ext::AlignExt;
@@ -965,7 +966,36 @@ impl<C: PagingConstsTrait> AbstractVaddr<C> {
             self.rec_compute_vaddr(start) as int == self.to_vaddr_indices(start) + self.offset,
         decreases C::NR_LEVELS() - start,
     {
-        admit();
+        vstd::arithmetic::power2::lemma2_to64();
+        vstd::arithmetic::power2::lemma2_to64_rest();
+        lemma_page_size_spec_values();
+        vstd_extra::external::ilog2::lemma_usize_ilog2_to32();
+        C::lemma_paging_consts_properties();
+        assert(nr_subpage_per_huge::<C>() == NR_ENTRIES);
+        self.to_vaddr_indices_gap_bound(start);
+        if start < C::NR_LEVELS() {
+            self.rec_compute_vaddr_is_to_vaddr_indices(start + 1);
+            self.to_vaddr_indices_gap_bound(start + 1);
+            assert(self.index.contains_key(start));
+            // page_size(start+1) matches the positional shift pow2(12 + 9*start).
+            // For NR_LEVELS == 4, enumerate concrete cases so the constant
+            // folds from `lemma_page_size_spec_values`.
+            // With nr_subpage_per_huge::<C>() == NR_ENTRIES == nr_subpage_per_huge::<PagingConsts>(),
+            // page_size::<C>(n) == page_size::<PagingConsts>(n).
+            if start == 0 {
+                assert(page_size::<C>(1) == page_size::<PagingConsts>(1));
+                assert(page_size::<C>(1) == pow2(12nat) as usize);
+            } else if start == 1 {
+                assert(page_size::<C>(2) == page_size::<PagingConsts>(2));
+                assert(page_size::<C>(2) == pow2(21nat) as usize);
+            } else if start == 2 {
+                assert(page_size::<C>(3) == page_size::<PagingConsts>(3));
+                assert(page_size::<C>(3) == pow2(30nat) as usize);
+            } else {
+                assert(page_size::<C>(4) == page_size::<PagingConsts>(4));
+                assert(page_size::<C>(4) == pow2(39nat) as usize);
+            }
+        }
     }
 
     /// Full identity relating `to_vaddr()` to `compute_vaddr()`:

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

@@ -448,7 +448,51 @@ impl<C: PageTableConfig> EntryOwner<C> {
                 (self.parent_level - 1) as PagingLevel,
             )) as Paddr) % PAGE_SIZE == 0,
     {
-        admit();
+        let pa = self.frame().mapped_pa;
+        let child_pa = (pa + idx * page_size::<C>((self.parent_level - 1) as PagingLevel)) as Paddr;
+        C::lemma_paging_consts_properties();
+        assert(C::NR_LEVELS() == NR_LEVELS);
+        assert(self.parent_level == 2 || self.parent_level == 3);
+        assert(NR_ENTRIES == 512) by {
+            crate::arch::mm::lemma_nr_subpage_per_huge_eq_nr_entries();
+        };
+        assert(crate::mm::nr_subpage_per_huge::<C>() == 512usize) by {
+            C::lemma_paging_consts_properties();
+        };
+        vstd_extra::external::ilog2::lemma_usize_ilog2_to32();
+        crate::specs::mm::page_table::cursor::page_size_lemmas::lemma_page_size_spec_level1::<C>();
+        assert(512usize.ilog2() == 9);
+        vstd::arithmetic::power2::lemma2_to64();
+        if self.parent_level == 2 {
+            assert(page_size::<C>(2) == (PAGE_SIZE * pow2((512usize.ilog2() * 1usize) as nat)) as usize);
+            assert(page_size::<C>(2) == 2097152);
+            assert(pa % page_size::<C>(2) == 0);
+            crate::specs::mm::page_table::cursor::page_size_lemmas::lemma_page_size_divides::<C>(1, 2);
+            assert(child_pa % page_size::<C>(1) == 0);
+            assert(child_pa + page_size::<C>(1) <= MAX_PADDR) by {
+                assert(idx < 512);
+                assert(idx * 4096 + 4096 <= 2097152);
+                assert(child_pa + page_size::<C>(1) <= pa + page_size::<C>(2));
+            };
+        } else {
+            assert(self.parent_level == 3);
+            assert(page_size::<C>(3) == (PAGE_SIZE * pow2((512usize.ilog2() * 2usize) as nat)) as usize);
+            assert(page_size::<C>(3) == 1073741824);
+            assert(pa % page_size::<C>(3) == 0);
+            crate::specs::mm::page_table::cursor::page_size_lemmas::lemma_va_align_page_size::<C>(pa, 2);
+            assert(child_pa == pa + idx * page_size::<C>(2));
+            vstd::arithmetic::div_mod::lemma_mod_multiples_basic(idx as int, page_size::<C>(2) as int);
+            vstd::arithmetic::div_mod::lemma_add_mod_noop(
+                pa as int,
+                (idx * page_size::<C>(2)) as int,
+                page_size::<C>(2) as int,
+            );
+            assert(child_pa % page_size::<C>(2) == 0);
+            assert(child_pa + page_size::<C>(2) <= MAX_PADDR) by {
+                assert(idx * 2097152 + 2097152 <= 1073741824);
+                assert(child_pa + page_size::<C>(2) <= pa + page_size::<C>(3));
+            };
+        }
     }
 
     /// Helper: sub-page validity is preserved when the only slot that changed is the

ostd/specs/mm/page_table/owners.rs

@@ -14,7 +14,7 @@ use vstd_extra::ownership::*;
 use vstd_extra::prelude::TreeNodeValue;
 
 use crate::mm::{
-    Paddr, PagingLevel, Vaddr, page_size,
+    MAX_NR_LEVELS, Paddr, PagingConstsTrait, PagingLevel, Vaddr, page_size,
     page_table::{EntryOwner, EntryOwnerKind},
 };
 
@@ -115,6 +115,7 @@ pub proof fn lemma_leading_bits_bounded<C: PageTableConfig>()
     C::lemma_leading_bits_bounded();
 }
 
+
 /// `vaddr(path) < 2^48` for every valid path: each term in the positional
 /// sum is `i_k * 2^(12 + 9·k)` with `i_k < 512 = 2^9`, so the sum is
 /// strictly less than `2^48`.
@@ -141,11 +142,11 @@ pub proof fn lemma_vaddr_of_eq_int<C: PageTableConfig>(path: TreePath<NR_ENTRIES
             * 0x1_0000_0000_0000int,
 {
     lemma_leading_bits_bounded::<C>();
+    C::lemma_page_table_config_constant_requirements();
     lemma_vaddr_strict_bound::<C>(path);
     let lb = C::LEADING_BITS_spec() as int;
     let v = vaddr::<C>(path) as int;
     // `0 <= v + lb * 2^48 < 2^64`: sum fits in usize, cast is lossless.
-    assert(0 <= v);
     assert(lb * 0x1_0000_0000_0000int <= 0xffff_int * 0x1_0000_0000_0000int) by (nonlinear_arith)
         requires
             lb < 0x1_0000int,
@@ -159,6 +160,37 @@ pub proof fn lemma_vaddr_of_eq_int<C: PageTableConfig>(path: TreePath<NR_ENTRIES
     ;
 }
 
+/// page_size is monotonically increasing in its argument.
+pub proof fn page_size_monotonic<C: PagingConstsTrait>(a: PagingLevel, b: PagingLevel)
+    requires
+        1 <= a <= b <= C::NR_LEVELS() + 1,
+    ensures
+        page_size::<C>(a) <= page_size::<C>(b),
+{
+    if a == b {
+    } else {
+        let ps_a = page_size::<C>(a);
+        let ps_b = page_size::<C>(b);
+
+        lemma_page_size_ge_page_size::<C>(a);
+        lemma_page_size_ge_page_size::<C>(b);
+        C::lemma_paging_consts_properties();
+
+        lemma_page_size_divides::<C>(a, b);
+        assert(ps_b % ps_a == 0);
+
+        assert(ps_a <= ps_b) by {
+            if ps_b < ps_a {
+                vstd::arithmetic::div_mod::lemma_small_mod(ps_b as nat, ps_a as nat);
+                assert(ps_b % ps_a == ps_b);
+                assert(ps_b % ps_a == 0);
+                assert(false);
+            }
+        }
+    }
+}
+
+
 /// Sibling paths (same prefix, different last index) have disjoint VA ranges,
 /// separated by at least the child page size.
 ///
@@ -1384,6 +1416,7 @@ impl<C: PageTableConfig> PageTableOwner<C> {
             // Bridge `vaddr_of(path) as int == vaddr(path) + LB * 2^48`.
             lemma_vaddr_of_eq_int::<C>(path);
             lemma_leading_bits_bounded::<C>();
+            C::lemma_page_table_config_constant_requirements();
             lemma_vaddr_strict_bound::<C>(path);
             let lb = C::LEADING_BITS_spec() as int;
             vstd::arithmetic::power2::lemma2_to64();