Skip to content

Commit 6e08e3c

Browse files
hiroki-chenhiroki-chen
committed
Merge branch 'phaseII/verified' of github.com:asterinas/vostd into phaseII/verified
2 parents 9779ebd + 5f5e6be commit 6e08e3c

10 files changed

Lines changed: 63 additions & 129 deletions

File tree

‎ostd/specs/mm/page_table/node/child.rs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -52,7 +52,7 @@ impl<'a, C: PageTableConfig> OwnerOf for ChildRef<'a, C> {
5252
Self::None => owner.is_absent(),
5353
}
5454
}
55-
}
55+
}
5656

5757
impl<C: PageTableConfig> Child<C> {
5858

‎ostd/specs/mm/page_table/node/entry_owners.rs‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ use crate::mm::frame::meta::REF_COUNT_UNUSED;
1111
use crate::mm::page_prop::PageProperty;
1212
use crate::mm::page_table::*;
1313
use crate::mm::{Paddr, PagingConstsTrait, PagingLevel, Vaddr};
14+
use crate::mm::frame::meta::REF_COUNT_UNUSED;
1415
use crate::specs::arch::mm::{NR_ENTRIES, NR_LEVELS, PAGE_SIZE};
1516
use crate::specs::arch::paging_consts::PagingConsts;
1617
use crate::specs::arch::*;

‎ostd/specs/mm/page_table/node/owners.rs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -106,7 +106,7 @@ impl<C: PageTableConfig> Inv for NodeOwner<C> {
106106
impl<C: PageTableConfig> NodeOwner<C> {
107107
/// Returns a NodeOwner with children_perm updated at the given index.
108108
/// Used to specify the state after storing a new PTE for an allocated child.
109-
pub uninterp spec fn set_children_perm(self, idx: usize, pte: C::E) -> Self;
109+
pub open spec fn set_children_perm(self, idx: usize, pte: C::E) -> Self;
110110

111111
#[verifier::external_body]
112112
pub axiom fn set_children_perm_axiom(self, idx: usize, pte: C::E)

‎ostd/specs/mm/page_table/owners.rs‎

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -13,10 +13,13 @@ use vstd_extra::ghost_tree::*;
1313
use vstd_extra::ownership::*;
1414
use vstd_extra::prelude::TreeNodeValue;
1515

16-
use crate::mm::{page_table::EntryOwner, Paddr, PagingLevel, Vaddr, MAX_NR_LEVELS};
16+
use crate::mm::{
17+
page_table::EntryOwner,
18+
Paddr, PagingLevel, Vaddr, MAX_NR_LEVELS,
19+
};
1720

1821
use crate::mm::frame::frame_to_index;
19-
use crate::mm::page_table::{PageTableEntryTrait, PageTableGuard};
22+
use crate::mm::page_table::{PageTableGuard, PageTableEntryTrait};
2023

2124
use crate::specs::arch::*;
2225
use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;

‎ostd/src/mm/frame/frame_ref.rs‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -67,7 +67,6 @@ impl<M: AnyFrameMeta> FrameRef<'_, M> {
6767
pub(in crate::mm) fn borrow_paddr(raw: Paddr) -> Self {
6868
proof {
6969
broadcast use crate::mm::frame::meta::mapping::group_page_meta;
70-
7170
old(regions).inv_implies_correct_addr(raw);
7271
}
7372

‎ostd/src/mm/frame/mod.rs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -417,8 +417,8 @@ impl<'a, M: AnyFrameMeta> Frame<M> {
417417
pub fn borrow(&self) -> FrameRef<'a, M> {
418418
assert(regions.slot_owners.contains_key(self.index()));
419419
broadcast use crate::mm::frame::meta::mapping::group_page_meta;
420-
// SAFETY: Both the lifetime and the type matches `self`.
421420

421+
// SAFETY: Both the lifetime and the type matches `self`.
422422
#[verus_spec(with Tracked(&perm.points_to))]
423423
let paddr = self.start_paddr();
424424

‎ostd/src/mm/page_table/cursor/mod.rs‎

Lines changed: 15 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -42,9 +42,7 @@ use crate::mm::frame::Frame;
4242
use crate::mm::page_table::*;
4343
use crate::mm::{Paddr, Vaddr, MAX_NR_LEVELS};
4444
use crate::specs::arch::kspace::FRAME_METADATA_RANGE;
45-
use crate::specs::mm::frame::mapping::{
46-
frame_to_index, frame_to_meta, meta_to_frame, META_SLOT_SIZE,
47-
};
45+
use crate::specs::mm::frame::mapping::{frame_to_index, frame_to_meta, meta_to_frame, META_SLOT_SIZE};
4846
use crate::specs::mm::frame::meta_owners::{MetaSlotOwner, REF_COUNT_UNUSED};
4947
use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;
5048

@@ -1358,6 +1356,7 @@ impl<'rcu, C: PageTableConfig, A: InAtomicMode> CursorMut<'rcu, C, A> {
13581356
self.inner.guard_level == old(self).inner.guard_level,
13591357
)]
13601358
fn map_branch_none(&mut self, cur_entry: &mut Entry<'rcu, C>, rcu_guard: &'rcu A) {
1359+
13611360
let ghost owner0 = *owner;
13621361
let ghost guards0 = *guards;
13631362

@@ -1457,9 +1456,7 @@ impl<'rcu, C: PageTableConfig, A: InAtomicMode> CursorMut<'rcu, C, A> {
14571456
0 <= j < NR_ENTRIES
14581457
&& cont.children[j] is Some implies cont.children[j].unwrap().tree_predicate_map(
14591458
cont.path().push_tail(j as usize), g_region) by {
1460-
assert(OwnerSubtree::implies(f_region, g_region)) by {
1461-
admit();
1462-
}
1459+
assert(OwnerSubtree::implies(f_region, g_region)) by { admit(); }
14631460
OwnerSubtree::map_implies(
14641461
cont.children[j].unwrap(),
14651462
cont.path().push_tail(j as usize),
@@ -1476,9 +1473,7 @@ impl<'rcu, C: PageTableConfig, A: InAtomicMode> CursorMut<'rcu, C, A> {
14761473
&& cont_final.children[j] is Some implies cont_final.children[j].unwrap().tree_predicate_map(
14771474
cont_final.path().push_tail(j as usize), g_region) by {
14781475
if j != idx && cont0.children[j] is Some {
1479-
assert(OwnerSubtree::implies(f_region, g_region)) by {
1480-
admit();
1481-
}
1476+
assert(OwnerSubtree::implies(f_region, g_region)) by { admit(); }
14821477
OwnerSubtree::map_implies(
14831478
cont0.children[j].unwrap(),
14841479
cont0.path().push_tail(j as usize),
@@ -1493,9 +1488,7 @@ impl<'rcu, C: PageTableConfig, A: InAtomicMode> CursorMut<'rcu, C, A> {
14931488
}
14941489

14951490
proof {
1496-
assert(owner.relate_region(*regions)) by {
1497-
admit();
1498-
}
1491+
assert(owner.relate_region(*regions)) by { admit(); }
14991492
}
15001493

15011494
#[verus_spec(with Tracked(owner), Tracked(guard_perm.tracked_unwrap()), Tracked(regions), Tracked(guards))]
@@ -1635,9 +1628,7 @@ impl<'rcu, C: PageTableConfig, A: InAtomicMode> CursorMut<'rcu, C, A> {
16351628
},
16361629
ChildRef::None => {
16371630
proof {
1638-
assert(owner.level > 2) by {
1639-
admit();
1640-
}
1631+
assert(owner.level > 2) by { admit(); }
16411632
}
16421633
#[verus_spec(with Tracked(owner), Tracked(regions), Tracked(guards))]
16431634
self.map_branch_none(&mut cur_entry, rcu_guard);
@@ -1686,7 +1677,8 @@ impl<'rcu, C: PageTableConfig, A: InAtomicMode> CursorMut<'rcu, C, A> {
16861677
&&& self.inner.va % page_size(level) == 0
16871678
&&& self.inner.va + page_size(level) <= self.inner.barrier_va.end
16881679
&&& level < self.inner.guard_level
1689-
&&& (entry_owner.is_absent() || Child::Frame(paddr, level, prop).wf(entry_owner))
1680+
&&& (entry_owner.is_absent()
1681+
|| Child::Frame(paddr, level, prop).wf(entry_owner))
16901682
}
16911683

16921684
pub open spec fn item_not_mapped(item: C::Item, regions: MetaRegionOwners) -> bool {
@@ -2042,17 +2034,16 @@ impl<'rcu, C: PageTableConfig, A: InAtomicMode> CursorMut<'rcu, C, A> {
20422034
!old(owner).popped_too_high,
20432035
new_owner.inv(),
20442036
new_owner.level == old(owner).continuations[old(owner).level - 1].tree_level + 1,
2045-
new_owner.value.parent_level == old(owner).continuations[old(owner).level
2046-
- 1].child().value.parent_level,
2037+
new_owner.value.parent_level == old(owner).continuations[old(owner).level - 1].child().value.parent_level,
20472038
new_owner.value.path == old(owner).continuations[old(owner).level - 1].path().push_tail(
20482039
old(owner).continuations[old(owner).level - 1].idx as usize,
20492040
),
20502041
new_child.wf(new_owner.value),
2051-
new_owner.value.is_node() ==> old(regions).slot_owners[frame_to_index(
2052-
new_owner.value.meta_slot_paddr().unwrap(),
2053-
)].inner_perms.ref_count.value() != REF_COUNT_UNUSED,
2042+
new_owner.value.is_node() ==> old(regions).slot_owners[
2043+
frame_to_index(new_owner.value.meta_slot_paddr().unwrap())
2044+
].inner_perms.ref_count.value() != REF_COUNT_UNUSED,
20542045
new_owner.value.is_node() ==> old(regions).slots.contains_key(
2055-
frame_to_index(new_owner.value.meta_slot_paddr().unwrap()),
2046+
frame_to_index(new_owner.value.meta_slot_paddr().unwrap())
20562047
),
20572048
new_owner.value.in_scope,
20582049
new_owner.value.relate_region(*old(regions)),
@@ -2152,9 +2143,8 @@ impl<'rcu, C: PageTableConfig, A: InAtomicMode> CursorMut<'rcu, C, A> {
21522143

21532144
assert(new_owner.value.meta_slot_paddr() == pre_new_owner_value.meta_slot_paddr());
21542145
let f_neq = |entry: EntryOwner<C>, path: TreePath<NR_ENTRIES>|
2155-
entry.meta_slot_paddr_neq(pre_new_owner_value) && entry.meta_slot_paddr_neq(
2156-
old_child_owner.value,
2157-
);
2146+
entry.meta_slot_paddr_neq(pre_new_owner_value)
2147+
&& entry.meta_slot_paddr_neq(old_child_owner.value);
21582148
let f_region = PageTableOwner::<C>::relate_region_pred(regions0);
21592149
let g_region = PageTableOwner::<C>::relate_region_pred(*regions);
21602150
let f_path = PageTableOwner::<C>::path_tracked_pred(regions0);

‎ostd/src/mm/page_table/node/child.rs‎

Lines changed: 9 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -2,9 +2,9 @@
22
//! This module specifies the type of the children of a page table node.
33
use vstd::prelude::*;
44

5-
use crate::mm::frame::meta::has_safe_slot;
65
use crate::mm::frame::meta::mapping::{frame_to_index, frame_to_meta, meta_addr, meta_to_frame};
76
use crate::mm::frame::Frame;
7+
use crate::mm::frame::meta::has_safe_slot;
88
use crate::mm::page_table::*;
99
use crate::specs::arch::mm::{NR_ENTRIES, NR_LEVELS, PAGE_SIZE};
1010
use crate::specs::arch::paging_consts::PagingConsts;
@@ -70,9 +70,8 @@ impl<C: PageTableConfig> Child<C> {
7070
owner.pte_invariants(res, *regions),
7171
*regions == old(owner).into_pte_regions_spec(*old(regions)),
7272
*owner == old(owner).into_pte_owner_spec(),
73-
old(owner).node is Some ==> res == C::E::new_pt_spec(
74-
meta_to_frame(old(owner).node.unwrap().meta_perm.addr()),
75-
),
73+
old(owner).node is Some ==>
74+
res == C::E::new_pt_spec(meta_to_frame(old(owner).node.unwrap().meta_perm.addr())),
7675
{
7776
proof {
7877
C::E::new_properties();
@@ -99,20 +98,17 @@ impl<C: PageTableConfig> Child<C> {
9998
C::E::new_pt(paddr)
10099
},
101100
Child::Frame(paddr, level, prop) => {
102-
proof {
103-
owner.in_scope = false;
104-
}
101+
proof { owner.in_scope = false; }
105102
C::E::new_page(paddr, level, prop)
106103
},
107104
Child::None => {
108-
proof {
109-
owner.in_scope = false;
110-
}
105+
proof { owner.in_scope = false; }
111106
C::E::new_absent()
112107
},
113108
}
114109
}
115110

111+
116112
/// Converts a `PTE` to a `Child`.
117113
///
118114
/// # Verified Properties
@@ -142,17 +138,14 @@ impl<C: PageTableConfig> Child<C> {
142138
*regions == entry_own.from_pte_regions_spec(*old(regions)),
143139
{
144140
if !pte.is_present() {
145-
proof {
146-
entry_own.in_scope = true;
147-
}
141+
proof { entry_own.in_scope = true; }
148142
return Child::None;
149143
}
150144
let paddr = pte.paddr();
151145

152146
if !pte.is_last(level) {
153147
proof {
154148
broadcast use crate::mm::frame::meta::mapping::group_page_meta;
155-
156149
regions.inv_implies_correct_addr(paddr);
157150
}
158151

@@ -162,17 +155,13 @@ impl<C: PageTableConfig> Child<C> {
162155
proof {
163156
entry_own.in_scope = true;
164157

165-
assert(regions.slot_owners =~= entry_own.from_pte_regions_spec(
166-
*old(regions),
167-
).slot_owners);
158+
assert(regions.slot_owners =~= entry_own.from_pte_regions_spec(*old(regions)).slot_owners);
168159
assert(regions.slots =~= entry_own.from_pte_regions_spec(*old(regions)).slots);
169160
}
170161

171162
return Child::PageTable(node);
172163
}
173-
proof {
174-
entry_own.in_scope = true;
175-
}
164+
proof { entry_own.in_scope = true; }
176165
Child::Frame(paddr, level, pte.prop())
177166
}
178167
}
@@ -227,7 +216,6 @@ impl<C: PageTableConfig> ChildRef<'_, C> {
227216
if !pte.is_last(level) {
228217
proof {
229218
broadcast use crate::mm::frame::meta::mapping::group_page_meta;
230-
231219
regions.inv_implies_correct_addr(paddr);
232220
}
233221

0 commit comments

Comments
 (0)