Aligen definitions with corter-3 (#78)

* Rename Cursor fields

* More rename

* Align with asterinas definition of PagingConstsTrait

* fmt

* fmt

Author: rikosellic

lock-protocol/src/exec/rw/common.rs

@@ -13,15 +13,10 @@ use crate::helpers::extern_const::*;
 use crate::spec::{common::*, utils::*};
 
 pub use super::configs::*;
+pub use crate::mm::{Paddr, Vaddr, PagingLevel};
 
 verus! {
 
-pub type Paddr = usize;
-
-pub type Vaddr = usize;
-
-pub type PagingLevel = usize;
-
 // pub const MAX_FRAME_NUM: u64 = 256;
 pub const INVALID_PADDR: Paddr = 0xffff_ffff_ffff_ffff;
 

lock-protocol/src/exec/rw/cursor.rs

@@ -24,19 +24,20 @@ use crate::mm::page_table::cursor::MAX_NR_LEVELS;
 verus! {
 
 pub enum GuardInPath {
-    ReadLocked(PageTableReadLock),
-    WriteLocked(PageTableWriteLock),
-    None,
+    Read(PageTableReadLock),
+    Write(PageTableWriteLock),
+    ImplicitWrite(PageTableWriteLock),
+    Unlocked,
 }
 
 impl GuardInPath {
     #[verifier::external_body]  // Verus does not support replace.
     pub fn take(&mut self) -> (res: Self)
         ensures
             res =~= *old(self),
-            *self is None,
+            *self is Unlocked,
     {
-        core::mem::replace(self, Self::None)
+        core::mem::replace(self, Self::Unlocked)
     }
 }
 
@@ -58,15 +59,15 @@ impl Cursor {
             #![trigger self.path[level - 1]]
             1 <= level <= 4 ==> {
                 if level < self.guard_level {
-                    self.path[level - 1] is None
+                    self.path[level - 1] is Unlocked
                 } else if level == self.guard_level {
-                    &&& self.path[level - 1] is WriteLocked
-                    &&& self.path[level - 1]->WriteLocked_0.wf()
-                    &&& self.path[level - 1]->WriteLocked_0.inst_id() == self.inst@.id()
+                    &&& self.path[level - 1] is Write
+                    &&& self.path[level - 1]->Write_0.wf()
+                    &&& self.path[level - 1]->Write_0.inst_id() == self.inst@.id()
                 } else {
-                    &&& self.path[level - 1] is ReadLocked
-                    &&& self.path[level - 1]->ReadLocked_0.wf()
-                    &&& self.path[level - 1]->ReadLocked_0.inst_id() == self.inst@.id()
+                    &&& self.path[level - 1] is Read
+                    &&& self.path[level - 1]->Read_0.wf()
+                    &&& self.path[level - 1]->Read_0.inst_id() == self.inst@.id()
                 }
             }
             // &&& valid_vaddr(self.va)
@@ -88,7 +89,7 @@ impl Cursor {
         &&& self.unlock_level@ == 5
         &&& forall|level: int|
             #![trigger self.path@[level - 1]]
-            1 <= level <= 4 ==> self.path@[level - 1] is None
+            1 <= level <= 4 ==> self.path@[level - 1] is Unlocked
     }
 
     pub open spec fn wf_with_lock_protocol_model(&self, m: LockProtocolModel) -> bool {
@@ -97,11 +98,12 @@ impl Cursor {
         &&& forall|level: int|
             #![trigger self.path[level - 1]]
             self.unlock_level@ <= level <= 4 ==> {
-                &&& !(self.path[level - 1] is None)
+                &&& !(self.path[level - 1] is Unlocked)
                 &&& match self.path[level - 1] {
-                    GuardInPath::ReadLocked(rguard) => m.path()[4 - level] == rguard.nid(),
-                    GuardInPath::WriteLocked(wguard) => m.path()[4 - level] == wguard.nid(),
-                    GuardInPath::None => true,
+                    GuardInPath::Read(rguard) => m.path()[4 - level] == rguard.nid(),
+                    GuardInPath::Write(wguard) => m.path()[4 - level] == wguard.nid(),
+                    GuardInPath::ImplicitWrite(wguard) => m.path()[4 - level] == wguard.nid(),
+                    GuardInPath::Unlocked => true,
                 }
             }
     }
@@ -112,7 +114,7 @@ impl Cursor {
             0 <= idx < old(self).path@.len(),
         ensures
             res =~= old(self).path@[idx as int],
-            self.path@ =~= old(self).path@.update(idx as int, GuardInPath::None),
+            self.path@ =~= old(self).path@.update(idx as int, GuardInPath::Unlocked),
             self.level == old(self).level,
             self.guard_level == old(self).guard_level,
             self.va =~= old(self).va,
@@ -254,10 +256,10 @@ pub fn lock_range(
         res.0.wf_with_lock_protocol_model(res.1@),
 {
     let mut path: [GuardInPath; MAX_NR_LEVELS] = [
-        GuardInPath::None,
-        GuardInPath::None,
-        GuardInPath::None,
-        GuardInPath::None,
+        GuardInPath::Unlocked,
+        GuardInPath::Unlocked,
+        GuardInPath::Unlocked,
+        GuardInPath::Unlocked,
     ];
 
     let ghost mut cur_nid: NodeId = 0;
@@ -303,12 +305,12 @@ pub fn lock_range(
             forall|i: int|
                 #![trigger path@[i - 1]]
                 level < i <= 4 ==> {
-                    &&& path@[i - 1] is ReadLocked
-                    &&& path@[i - 1]->ReadLocked_0.wf()
-                    &&& path@[i - 1]->ReadLocked_0.inst_id() == pt.inst@.id()
-                    &&& m.path()[4 - i] == path@[i - 1]->ReadLocked_0.nid()
+                    &&& path@[i - 1] is Read
+                    &&& path@[i - 1]->Read_0.wf()
+                    &&& path@[i - 1]->Read_0.inst_id() == pt.inst@.id()
+                    &&& m.path()[4 - i] == path@[i - 1]->Read_0.nid()
                 },
-            forall|i: int| #![trigger path@[i - 1]] 1 <= i <= level ==> path@[i - 1] is None,
+            forall|i: int| #![trigger path@[i - 1]] 1 <= i <= level ==> path@[i - 1] is Unlocked,
             m.path().len() == 4 - level,
             m.path().is_prefix_of(va_range_get_tree_path(*va)),
             m.state() is ReadLocking,
@@ -327,12 +329,12 @@ pub fn lock_range(
             forall|i: int|
                 #![trigger path@[i - 1]]
                 level < i <= 4 ==> {
-                    &&& path@[i - 1] is ReadLocked
-                    &&& path@[i - 1]->ReadLocked_0.wf()
-                    &&& path@[i - 1]->ReadLocked_0.inst_id() == pt.inst@.id()
-                    &&& m.path()[4 - i] == path@[i - 1]->ReadLocked_0.nid()
+                    &&& path@[i - 1] is Read
+                    &&& path@[i - 1]->Read_0.wf()
+                    &&& path@[i - 1]->Read_0.inst_id() == pt.inst@.id()
+                    &&& m.path()[4 - i] == path@[i - 1]->Read_0.nid()
                 },
-            forall|i: int| #![trigger path@[i - 1]] 1 <= i <= level ==> path@[i - 1] is None,
+            forall|i: int| #![trigger path@[i - 1]] 1 <= i <= level ==> path@[i - 1] is Unlocked,
             m.path().len() == 4 - level,
             m.path().is_prefix_of(va_range_get_tree_path(*va)),
             m.state() is ReadLocking,
@@ -393,7 +395,7 @@ pub fn lock_range(
         match child {
             Child::PageTable(_, _, _) => unreached(),
             Child::PageTableRef(pt, _, _) => {
-                path[level as usize - 1] = GuardInPath::ReadLocked(cur_pt_rlockguard);
+                path[level as usize - 1] = GuardInPath::Read(cur_pt_rlockguard);
                 cur_pt_paddr = pt;
                 level -= 1;
                 proof {
@@ -433,7 +435,7 @@ pub fn lock_range(
                             m = res.1.get();
                         }
 
-                        path[level as usize - 1] = GuardInPath::ReadLocked(cur_pt_rlockguard);
+                        path[level as usize - 1] = GuardInPath::Read(cur_pt_rlockguard);
                         cur_pt_paddr = pt;
                         level -= 1;
                         proof {
@@ -470,7 +472,7 @@ pub fn lock_range(
                         proof {
                             m = res.1.get();
                         }
-                        path[level as usize - 1] = GuardInPath::ReadLocked(cur_pt_rlockguard);
+                        path[level as usize - 1] = GuardInPath::Read(cur_pt_rlockguard);
                         level -= 1;
                         proof {
                             cur_nid = NodeHelper::get_child(cur_nid, start_idx as nat);
@@ -517,7 +519,7 @@ pub fn lock_range(
         res.0
     };
 
-    path[level as usize - 1] = GuardInPath::WriteLocked(cur_pt_wlockguard);
+    path[level as usize - 1] = GuardInPath::Write(cur_pt_wlockguard);
 
     let tracked inst = pt.inst.borrow().clone();
     let cursor = Cursor {
@@ -548,9 +550,9 @@ pub fn unlock_range(cursor: &mut Cursor, m: Tracked<LockProtocolModel>) -> (res:
     let tracked mut m = m.get();
 
     let guard_level = cursor.guard_level;
-    let GuardInPath::WriteLocked(mut guard_node) = cursor.take_guard(
-        guard_level as usize - 1,
-    ) else { unreached() };
+    let GuardInPath::Write(mut guard_node) = cursor.take_guard(guard_level as usize - 1) else {
+        unreached()
+    };
     let res = guard_node.unlock(Tracked(m));
     let pt = res.0;
     proof {
@@ -568,22 +570,22 @@ pub fn unlock_range(cursor: &mut Cursor, m: Tracked<LockProtocolModel>) -> (res:
             forall|level: int|
                 #![trigger cursor.path@[level - 1]]
                 i <= level <= 4 ==> {
-                    &&& cursor.path@[level - 1] is ReadLocked
-                    &&& cursor.path@[level - 1]->ReadLocked_0.wf()
-                    &&& cursor.path@[level - 1]->ReadLocked_0.inst_id() == cursor.inst@.id()
+                    &&& cursor.path@[level - 1] is Read
+                    &&& cursor.path@[level - 1]->Read_0.wf()
+                    &&& cursor.path@[level - 1]->Read_0.inst_id() == cursor.inst@.id()
                 },
             forall|level: int|
                 #![trigger cursor.path@[level - 1]]
-                1 <= level < i ==> cursor.path@[level - 1] is None,
+                1 <= level < i ==> cursor.path@[level - 1] is Unlocked,
             cursor.wf_with_lock_protocol_model(m),
             m.inv(),
             m.state() is ReadLocking,
             cursor.inst@.cpu_num() == GLOBAL_CPU_NUM,
         decreases 5 - i,
     {
         match cursor.take_guard(i as usize - 1) {
-            GuardInPath::None => unreached(),
-            GuardInPath::ReadLocked(mut rguard) => {
+            GuardInPath::Unlocked => unreached(),
+            GuardInPath::Read(mut rguard) => {
                 assert(m.path()[4 - i] == rguard.nid());
                 let res = rguard.unlock(Tracked(m));
                 let pt = res.0;
@@ -593,8 +595,8 @@ pub fn unlock_range(cursor: &mut Cursor, m: Tracked<LockProtocolModel>) -> (res:
                 pt.into_raw();
                 cursor.unlock_level = Ghost((cursor.unlock_level@ + 1) as PagingLevel);
             },
-            GuardInPath::WriteLocked(_) => unreached(),
-            // GuardInPath::ImplicitlyLocked(_) => unreached(),
+            GuardInPath::Write(_) => unreached(),
+            GuardInPath::ImplicitWrite(_) => unreached(),
         }
         i += 1;
     }

lock-protocol/src/mm/page_table/mod.rs

@@ -139,6 +139,38 @@ impl<C: PageTableConfig> PagingConstsTrait for C {
     fn NR_LEVELS() -> (res: PagingLevel) {
         C::C::NR_LEVELS()
     }
+
+    open spec fn HIGHEST_TRANSLATION_LEVEL_SPEC() -> PagingLevel {
+        C::C::HIGHEST_TRANSLATION_LEVEL_SPEC()
+    }
+
+    fn HIGHEST_TRANSLATION_LEVEL() -> PagingLevel {
+        C::C::HIGHEST_TRANSLATION_LEVEL()
+    }
+
+    open spec fn PTE_SIZE_SPEC() -> usize {
+        C::C::PTE_SIZE_SPEC()
+    }
+
+    fn PTE_SIZE() -> usize {
+        C::C::PTE_SIZE()
+    }
+
+    open spec fn ADDRESS_WIDTH_SPEC() -> usize {
+        C::C::ADDRESS_WIDTH_SPEC()
+    }
+
+    fn ADDRESS_WIDTH() -> usize {
+        C::C::ADDRESS_WIDTH()
+    }
+
+    open spec fn VA_SIGN_EXT_SPEC() -> bool {
+        C::C::VA_SIGN_EXT_SPEC()
+    }
+
+    fn VA_SIGN_EXT() -> bool {
+        C::C::VA_SIGN_EXT()
+    }
 }
 
 pub trait PageTableEntryTrait:
@@ -278,25 +310,61 @@ Sized {
 
     spec fn NR_LEVELS_SPEC() -> PagingLevel;
 
-    // /// The number of levels in the page table.
-    // /// The numbering of levels goes from deepest node to the root node. For example,
-    // /// the level 1 to 5 on AMD64 corresponds to Page Tables, Page Directory Tables,
-    // /// Page Directory Pointer Tables, Page-Map Level-4 Table, and Page-Map Level-5
-    // /// Table, respectively.
+    /// The number of levels in the page table.
+    /// The numbering of levels goes from deepest node to the root node. For example,
+    /// the level 1 to 5 on AMD64 corresponds to Page Tables, Page Directory Tables,
+    /// Page Directory Pointer Tables, Page-Map Level-4 Table, and Page-Map Level-5
+    /// Table, respectively.
     #[verifier::when_used_as_spec(NR_LEVELS_SPEC)]
     fn NR_LEVELS() -> PagingLevel
         returns
             Self::NR_LEVELS_SPEC(),
-    ;  // /
-    // The highest level that a PTE can be directly used to translate a VA.
-    // /// This affects the the largest page size supported by the page table.
-    // const HIGHEST_TRANSLATION_LEVEL: PagingLevel;
-    // /// The size of a PTE.
-    // const PTE_SIZE: usize;
-    // /// The address width may be BASE_PAGE_SIZE.ilog2() + NR_LEVELS * IN_FRAME_INDEX_BITS.
-    // /// If it is shorter than that, the higher bits in the highest level are ignored.
-    // const ADDRESS_WIDTH: usize;
+    ;
+
+    spec fn HIGHEST_TRANSLATION_LEVEL_SPEC() -> PagingLevel;
+
+    /// The highest level that a PTE can be directly used to translate a VA.
+    /// This affects the the largest page size supported by the page table.
+    #[verifier::when_used_as_spec(HIGHEST_TRANSLATION_LEVEL_SPEC)]
+    fn HIGHEST_TRANSLATION_LEVEL() -> PagingLevel
+        returns
+            Self::HIGHEST_TRANSLATION_LEVEL_SPEC(),
+    ;
+
+    spec fn PTE_SIZE_SPEC() -> usize;
+
+    /// The size of a PTE.
+    fn PTE_SIZE() -> usize
+        returns
+            Self::PTE_SIZE_SPEC(),
+    ;
 
+    spec fn ADDRESS_WIDTH_SPEC() -> usize;
+
+    /// The address width may be BASE_PAGE_SIZE.ilog2() + NR_LEVELS * IN_FRAME_INDEX_BITS.
+    /// If it is shorter than that, the higher bits in the highest level are ignored.
+    fn ADDRESS_WIDTH() -> usize
+        returns
+            Self::ADDRESS_WIDTH_SPEC(),
+    ;
+
+    spec fn VA_SIGN_EXT_SPEC() -> bool;
+
+    /// Whether virtual addresses are sign-extended.
+    ///
+    /// The sign bit of a [`Vaddr`] is the bit at index [`PagingConstsTrait::ADDRESS_WIDTH`] - 1.
+    /// If this constant is `true`, bits in [`Vaddr`] that are higher than the sign bit must be
+    /// equal to the sign bit. If an address violates this rule, both the hardware and OSTD
+    /// should reject it.
+    ///
+    /// Otherwise, if this constant is `false`, higher bits must be zero.
+    ///
+    /// Regardless of sign extension, [`Vaddr`] is always not signed upon calculation.
+    /// That means, `0xffff_ffff_ffff_0000 < 0xffff_ffff_ffff_0001` is `true`.
+    fn VA_SIGN_EXT() -> bool
+        returns
+            Self::VA_SIGN_EXT_SPEC(),
+    ;
 }
 
 // TODO: This is for x86, create the arch directory and move this to x86/mod.rs
@@ -323,10 +391,38 @@ impl PagingConstsTrait for PagingConsts {
     fn NR_LEVELS() -> (res: PagingLevel) {
         4
     }
-    // const ADDRESS_WIDTH: usize = 48;
-    // const HIGHEST_TRANSLATION_LEVEL: PagingLevel = 2;
-    // const PTE_SIZE: usize = core::mem::size_of::<PageTableEntry>();
 
+    open spec fn HIGHEST_TRANSLATION_LEVEL_SPEC() -> PagingLevel {
+        2
+    }
+
+    fn HIGHEST_TRANSLATION_LEVEL() -> PagingLevel {
+        2
+    }
+
+    open spec fn PTE_SIZE_SPEC() -> usize {
+        core::mem::size_of::<exec::SimplePageTableEntry>()
+    }
+
+    fn PTE_SIZE() -> usize {
+        core::mem::size_of::<exec::SimplePageTableEntry>()
+    }
+
+    open spec fn ADDRESS_WIDTH_SPEC() -> usize {
+        48
+    }
+
+    fn ADDRESS_WIDTH() -> usize {
+        48
+    }
+
+    open spec fn VA_SIGN_EXT_SPEC() -> bool {
+        true
+    }
+
+    fn VA_SIGN_EXT() -> bool {
+        true
+    }
 }
 
 // Copied from aster_common