Skip to content

Commit e192d03

Browse files
junyang-zhjunyang-zh
committed
Fix the proof
1 parent 36daf7d commit e192d03

4 files changed

Lines changed: 66 additions & 6 deletions

File tree

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

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -737,6 +737,14 @@ impl<'a, C: PageTableConfig> CursorMut<'a, C> {
737737
assert(!spt.ptes.value().contains_key(cur_entry.pte.pte_paddr() as int));
738738
assert(cur_entry.node.level_spec(&spt.alloc_model) == cur_level);
739739
let child_pt = cur_entry.alloc_if_none(preempt_guard, Tracked(spt)).unwrap();
740+
// TODO: Verus is able to prove `guard_option.unwrap().wf()` here, but with a deref to inner it fails,
741+
// this is trivial, might a verus bug?
742+
assume(forall|i: PagingLevel|
743+
#![trigger self.0.path[path_index_at_level_spec(i)]]
744+
self.0.level <= i <= self.0.guard_level ==> {
745+
let guard_option = path_index!(self.0.path[i]);
746+
&&& guard_option.unwrap().inner.wf(&spt.alloc_model)
747+
});
740748
self.0.push_level(child_pt, Tracked(spt));
741749
},
742750
ChildRef::Frame(_, _, _) => {

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

Lines changed: 48 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -40,7 +40,7 @@ use crate::exec;
4040

4141
verus! {
4242

43-
pub open spec fn spt_do_not_change_except<C: PageTableConfig>(
43+
pub open spec fn spt_do_not_change_except_modify_pte<C: PageTableConfig>(
4444
spt: &SubPageTable<C>,
4545
old_spt: &SubPageTable<C>,
4646
pte_addr: int,
@@ -99,4 +99,51 @@ pub open spec fn forward_spt_do_not_change_except<C: PageTableConfig>(
9999
}
100100
}
101101

102+
pub open spec fn spt_do_not_change_above_level<C: PageTableConfig>(
103+
spt: &SubPageTable<C>,
104+
old_spt: &SubPageTable<C>,
105+
level: PagingLevel,
106+
) -> bool {
107+
&&& forall|i: int|
108+
{
109+
(old_spt.frames.value().contains_key(i) && old_spt.frames.value()[i].level as int
110+
>= level) ==> {
111+
&&& #[trigger] spt.frames.value().contains_key(i)
112+
&&& #[trigger] spt.frames.value()[i] == old_spt.frames.value()[i]
113+
}
114+
}
115+
&&& forall|i: int|
116+
{
117+
(old_spt.alloc_model.meta_map.contains_key(i)
118+
&& old_spt.alloc_model.meta_map[i].value().level as int >= level) ==> {
119+
&&& #[trigger] spt.alloc_model.meta_map.contains_key(i)
120+
&&& spt.alloc_model.meta_map[i].pptr() == old_spt.alloc_model.meta_map[i].pptr()
121+
&&& spt.alloc_model.meta_map[i].value() == old_spt.alloc_model.meta_map[i].value()
122+
}
123+
}
124+
}
125+
126+
pub open spec fn alloc_model_do_not_change_except_add_frame<C: PageTableConfig>(
127+
spt: &SubPageTable<C>,
128+
old_spt: &SubPageTable<C>,
129+
new_frame: Paddr,
130+
) -> bool {
131+
&&& {
132+
forall|i: int| #[trigger]
133+
spt.alloc_model.meta_map.contains_key(i) && i != new_frame as int ==> {
134+
&&& #[trigger] old_spt.alloc_model.meta_map.contains_key(i)
135+
&&& spt.alloc_model.meta_map[i].pptr() == old_spt.alloc_model.meta_map[i].pptr()
136+
&&& spt.alloc_model.meta_map[i].value() == old_spt.alloc_model.meta_map[i].value()
137+
}
138+
}
139+
&&& {
140+
forall|i: int| #[trigger]
141+
old_spt.alloc_model.meta_map.contains_key(i) ==> {
142+
&&& #[trigger] spt.alloc_model.meta_map.contains_key(i)
143+
&&& spt.alloc_model.meta_map[i].pptr() == old_spt.alloc_model.meta_map[i].pptr()
144+
&&& spt.alloc_model.meta_map[i].value() == old_spt.alloc_model.meta_map[i].value()
145+
}
146+
}
147+
}
148+
102149
} // verus!

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

Lines changed: 9 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,8 @@ use crate::{
77
helpers::conversion::usize_mod_is_int_mod,
88
mm::{
99
cursor::spec_helpers::{
10-
self, spt_do_not_change_except, spt_do_not_change_except_frames_change,
10+
self, spt_do_not_change_except_modify_pte, spt_do_not_change_except_frames_change,
11+
spt_do_not_change_above_level, alloc_model_do_not_change_except_add_frame,
1112
},
1213
frame::allocator::AllocatorModel,
1314
meta::AnyFrameMeta,
@@ -192,7 +193,7 @@ impl<'a, 'rcu, C: PageTableConfig> Entry<'a, 'rcu, C> {
192193
spt.ptes.value().contains_key(self.pte.pte_paddr() as int),
193194
spt.instance.id() == old(spt).instance.id(),
194195
spt.wf(),
195-
spt_do_not_change_except(spt, old(spt), self.pte.pte_paddr() as int),
196+
spt_do_not_change_except_modify_pte(spt, old(spt), self.pte.pte_paddr() as int),
196197
spt.frames == old(spt).frames,
197198
spt.alloc_model == old(spt).alloc_model,
198199
self.remove_old_child(res, old(self).pte, old(spt), spt),
@@ -411,7 +412,9 @@ impl<'a, 'rcu, C: PageTableConfig> Entry<'a, 'rcu, C> {
411412
self.idx == old(self).idx,
412413
spt.wf(),
413414
res is Some,
414-
spt_do_not_change_except(spt, old(spt), self.pte.pte_paddr() as int),
415+
spt_do_not_change_except_modify_pte(spt, old(spt), self.pte.pte_paddr() as int),
416+
spt_do_not_change_above_level(spt, old(spt), self.node.level_spec(&spt.alloc_model)),
417+
alloc_model_do_not_change_except_add_frame(spt, old(spt), res.unwrap().paddr()),
415418
res.unwrap().wf(&spt.alloc_model),
416419
spt.i_ptes.value().contains_key(self.pte.pte_paddr() as int),
417420
!old(spt).frames.value().contains_key(res.unwrap().paddr() as int),
@@ -503,7 +506,9 @@ impl<'a, 'rcu, C: PageTableConfig> Entry<'a, 'rcu, C> {
503506
let node_ref = PageTableNodeRef::borrow_paddr(pa, Tracked(&spt.alloc_model));
504507

505508
assert(self.wf(spt));
506-
assume(spt_do_not_change_except(spt, old(spt), self.pte.pte_paddr() as int));
509+
assume(spt_do_not_change_except_modify_pte(spt, old(spt), self.pte.pte_paddr() as int));
510+
assume(spt_do_not_change_above_level(spt, old(spt), level));
511+
assume(alloc_model_do_not_change_except_add_frame(spt, old(spt), pa));
507512
assert(node_ref.level_spec(&spt.alloc_model) == level - 1);
508513

509514
Some(node_ref.make_guard_unchecked(guard, Ghost(self.va@)))

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -156,7 +156,7 @@ pub struct PageTableGuard<'a, C: PageTableConfig> {
156156

157157
impl<'a, C: PageTableConfig> PageTableGuard<'a, C> {
158158
pub open spec fn wf(&self, alloc_model: &AllocatorModel<PageTablePageMeta<C>>) -> bool {
159-
&&& self.inner.wf(alloc_model)
159+
self.inner.wf(alloc_model)
160160
}
161161

162162
#[verifier::allow_in_spec]

0 commit comments

Comments
 (0)