Format code

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

Author: zouyonghao

lock-protocol/src/mm/page_table/cursor/spec_helpers.rs

@@ -48,8 +48,9 @@ pub open spec fn spt_do_not_change_except_modify_pte<C: PageTableConfig>(
     &&& spt.wf()
     &&& old_spt.wf()
     &&& spt.instance.id() == old_spt.instance.id()
-    &&& spt.instance.root() == old_spt.instance.root()
-    // &&& forward_spt_do_not_change_except(spt, old_spt, pte_addr) // not correct?
+    &&& spt.instance.root()
+        == old_spt.instance.root()// &&& forward_spt_do_not_change_except(spt, old_spt, pte_addr)
+    // not correct?
     &&& forward_spt_do_not_change_except(old_spt, spt, pte_addr)
 }
 

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

@@ -120,14 +120,14 @@ impl<C: PageTableConfig> PageTableNode<C> {
             res.0.start_paddr() % page_size_spec::<C>(level) == 0,
             // old model does not change
             forall|pa: Paddr| #[trigger]
-                old(model).meta_map.contains_key(pa as int)
-                    <==> {
+                old(model).meta_map.contains_key(pa as int) <==> {
                     &&& #[trigger] model.meta_map.contains_key(pa as int)
                     &&& res.0.start_paddr() != pa
                 },
-            forall |pa: Paddr| #[trigger]
-                model.meta_map.contains_key(pa as int) && old(model).meta_map.contains_key(pa as int)
-                    ==> {
+            forall|pa: Paddr| #[trigger]
+                model.meta_map.contains_key(pa as int) && old(model).meta_map.contains_key(
+                    pa as int,
+                ) ==> {
                     &&& model.meta_map[pa as int] == old(model).meta_map[pa as int]
                 },
     {