Fix spt_do_not_change (#200)

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

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

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

Author: zouyonghao

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

@@ -583,7 +583,7 @@ impl<'a, C: PageTableConfig> Cursor<'a, C> {
             self.va == old(self).va,
             // Path remains unchanged except the one being set
             forall|i: PagingLevel|
-                #![trigger self.path.view().index(path_index_at_level_spec(i))]
+                #![auto]
                 old(self).level <= i <= old(self).guard_level ==> {
                     #[trigger] path_index!(self.path[i]) == path_index!(old(self).path[i])
                 },

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)
+    &&& 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/entry.rs

@@ -478,7 +478,7 @@ impl<'a, 'rcu, C: PageTableConfig> Entry<'a, 'rcu, C> {
                 map_va: self.va@ as int,
                 frame_pa: self.node.paddr() as int,
                 in_frame_index: self.idx as int,
-                map_to_pa: pt.start_paddr() as int,
+                map_to_pa: pa as int,
                 level,
                 phantom: PhantomData::<C>,
             };
@@ -498,7 +498,10 @@ impl<'a, 'rcu, C: PageTableConfig> Entry<'a, 'rcu, C> {
             }
             assert(spt.frames.value()[self.node.paddr() as int].level as int == level as int);
             spt.instance.set_child(i_pte, &mut spt.frames, &mut spt.i_ptes, &spt.ptes);
-            spt.perms.tracked_insert(pt.start_paddr(), perm);
+            spt.perms.tracked_insert(pa, perm);
+
+            // i_pte.entry_pa() == i_pte.pte_paddr_spec(). @see entry_pa
+            assert(spt.i_ptes.value().contains_key(self.pte.pte_paddr() as int));
         }
 
         assert(spt.wf());
@@ -514,12 +517,10 @@ impl<'a, 'rcu, C: PageTableConfig> Entry<'a, 'rcu, C> {
         assert(spt.alloc_model.meta_map.contains_key(pa as int));
         assert(spt.alloc_model.meta_map.contains_key(self.pte.frame_paddr() as int));
 
-        // assert(spt_do_not_change_except_modify_pte(spt, old(spt), self.pte.pte_paddr() as int));
-
         assert(self.wf(spt));
-        assume(spt_do_not_change_except_modify_pte(spt, old(spt), self.pte.pte_paddr() as int));
-        assume(spt_do_not_change_above_level(spt, old(spt), level));
-        assume(alloc_model_do_not_change_except_add_frame(spt, old(spt), pa));
+        assert(alloc_model_do_not_change_except_add_frame(spt, old(spt), pa));
+        assert(spt_do_not_change_above_level(spt, old(spt), level));
+        assert(spt_do_not_change_except_modify_pte(spt, old(spt), self.pte.pte_paddr() as int));
 
         let node_ref = PageTableNodeRef::borrow_paddr(pa, Tracked(&spt.alloc_model));
         assert(node_ref.level_spec(&spt.alloc_model) == level - 1);

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

@@ -120,9 +120,16 @@ 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)
-                    ==> #[trigger] model.meta_map.contains_key(pa as int)
-                    && model.meta_map[pa as int] == old(model).meta_map[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,
+                ) ==> {
+                    &&& model.meta_map[pa as int] == old(model).meta_map[pa as int]
+                },
     {
         crate::exec::alloc_page_table(level, Tracked(model))
     }

lock-protocol/src/spec/sub_pt/state_machine.rs

@@ -319,7 +319,20 @@ SubPageTableStateMachine<C: PageTableConfig> {
     }
 
     #[inductive(set_child)]
-    pub fn tr_set_child_invariant(pre: Self, post: Self, i_pte: IntermediatePageTableEntryView<C>) {}
+    pub fn tr_set_child_invariant(pre: Self, post: Self, i_pte: IntermediatePageTableEntryView<C>) {
+        assert(forall |i|
+            #[trigger] pre.frames.contains_key(i) ==>
+            (forall |l| #[trigger] pre.frames[i].ancestor_chain.dom().contains(l)
+            && !(#[trigger] pre.frames[i].ancestor_chain.index(l).entry_pa() == i_pte.entry_pa())) ==>
+               #[trigger] post.frames.contains_key(i)
+        );
+        // assert(forall |i|
+        //     #[trigger] post.frames.contains_key(i) ==>
+        //     (forall |l| #[trigger] post.frames[i].ancestor_chain.dom().contains(l)
+        //     && !(#[trigger] post.frames[i].ancestor_chain.index(l).entry_pa() == i_pte.entry_pa())) ==>
+        //        #[trigger] pre.frames.contains_key(i)
+        // );
+    }
 
     transition! {
         // remove a pte at a given address