Format code

Signed-off-by: Yonghao Zou <zouyonghao@live.cn>

Author: zouyonghao

lock-protocol/src/exec/mod.rs

@@ -147,7 +147,6 @@ pub fn alloc_page_table<C: PageTableConfig>(
 // //     fn is_last(&self, level: u8) -> bool {
 //         level == 1
 //     }
-
 ///    open spec fn is_last_spec(&self, level: PagingLevel) -> bool {
 ///        level == 1
 ///    }

lock-protocol/src/mm/frame/frame_ref.rs

@@ -4,7 +4,10 @@ use core::marker::PhantomData;
 use core::mem::ManuallyDrop;
 use core::ops::Deref;
 
-use crate::{mm::{cursor::MAX_NR_LEVELS, Paddr, PageTableConfig, PageTableNode, PagingConsts}, x86_64::NR_LEVELS_SPEC};
+use crate::{
+    mm::{cursor::MAX_NR_LEVELS, Paddr, PageTableConfig, PageTableNode, PagingConsts},
+    x86_64::NR_LEVELS_SPEC,
+};
 
 use super::{allocator::AllocatorModel, meta::AnyFrameMeta, Frame};
 use crate::mm::page_table::PagingConstsTrait;

lock-protocol/src/mm/page_table/node/child.rs

@@ -147,7 +147,8 @@ impl<'a, C: PageTableConfig> ChildRef<'a, C> {
             assert(node.wf(&spt.alloc_model));
             let res = ChildRef::PageTable(node);
             assert(spt.i_ptes.value().contains_key(entry.pte.pte_paddr() as int));
-            assert(node.level_spec(&spt.alloc_model) == entry.node.level_spec(&spt.alloc_model) - 1);
+            assert(node.level_spec(&spt.alloc_model) == entry.node.level_spec(&spt.alloc_model)
+                - 1);
             assert(res.child_entry_spt_wf(entry, spt));
             assert(!(res is None));
             assert(pte.is_present());

lock-protocol/src/mm/page_table/node/entry.rs

@@ -7,7 +7,8 @@ use crate::{
     helpers::conversion::usize_mod_is_int_mod,
     mm::{
         cursor::spec_helpers::{
-            self, alloc_model_do_not_change_except_add_frame, spt_do_not_change_above_level, spt_do_not_change_except_frames_change, spt_do_not_change_except_modify_pte
+            self, alloc_model_do_not_change_except_add_frame, spt_do_not_change_above_level,
+            spt_do_not_change_except_frames_change, spt_do_not_change_except_modify_pte,
         },
         frame::allocator::AllocatorModel,
         meta::AnyFrameMeta,
@@ -19,7 +20,8 @@ use crate::{
         NR_ENTRIES,
     },
     sync::rcu::RcuDrop,
-    task::DisabledPreemptGuard, x86_64::NR_LEVELS_SPEC,
+    task::DisabledPreemptGuard,
+    x86_64::NR_LEVELS_SPEC,
 };
 
 use super::{Child, ChildRef, PageTableGuard, PageTableNode, PageTableNodeRef};
@@ -83,17 +85,24 @@ impl<'a, 'rcu, C: PageTableConfig> Entry<'a, 'rcu, C> {
         &&& self.pte.is_present() <==> {
             &&& spt.alloc_model.meta_map.contains_key(self.pte.frame_paddr() as int)
         }
-        &&& forall |level: u8| self.pte.is_last(level) <==> {
-            spt.ptes.value().contains_key(self.pte.pte_paddr() as int) && level == 1
-        }
-        &&& forall |level: u8| !self.pte.is_last(level) <==> {
-            &&& #[trigger] spt.i_ptes.value().contains_key(#[trigger] self.pte.pte_paddr_spec() as int)
-            &&& level == self.node.level_spec(&spt.alloc_model)
-            &&& #[trigger] level_is_in_range::<C>(level as int)
-            // When this is an intermediate PTE, the child frame's level should be one less than current node's level
-            &&& spt.alloc_model.meta_map.contains_key(self.pte.frame_paddr() as int)
-            &&& spt.alloc_model.meta_map[self.pte.frame_paddr() as int].value().level == level - 1
-        }
+        &&& forall|level: u8|
+            self.pte.is_last(level) <==> {
+                spt.ptes.value().contains_key(self.pte.pte_paddr() as int) && level == 1
+            }
+        &&& forall|level: u8|
+            !self.pte.is_last(level) <==> {
+                &&& #[trigger] spt.i_ptes.value().contains_key(
+                    #[trigger] self.pte.pte_paddr_spec() as int,
+                )
+                &&& level == self.node.level_spec(&spt.alloc_model)
+                &&& #[trigger] level_is_in_range::<C>(
+                    level as int,
+                )
+                // When this is an intermediate PTE, the child frame's level should be one less than current node's level
+                &&& spt.alloc_model.meta_map.contains_key(self.pte.frame_paddr() as int)
+                &&& spt.alloc_model.meta_map[self.pte.frame_paddr() as int].value().level == level
+                    - 1
+            }
     }
 
     #[verifier::external_body]