Skip to content

Commit dddf63c

Browse files
SNoAndhiroki-chen
SNoAnd
and
hiroki-chen
authored
Frame documentation, pcell migration (#326)
* `ghost` into `tracked` for API compatibility * Support for `Once` * Update * vmio: initial layout * vmio: fix two issues with verus updates * stage * Fix `replace` to use parent node owner * Switch `FramePerm` to `MetaPerm` * Wrapper around `ManuallyDrop::new()` for cases when it is taking on the role of `into_raw` * vmio: more APIs * Fixup remaining proofs after `NeverDrop` change * Closing various unneessary admits in `cursor.rs` * Starting virtual pointer work * More cursor work * minor updates * Fix merge * Fix a verification error * Remove a file * `replace_cur_entry` * Update dv * Starting on virt_ptr * Migrating out of aster_common: vm_space * Migrate from aster_common: io, untyped, pod * Move specs into main ostd tree * Move `aster_common` into `ostd`, just in its own directory for now. * start vmspace stuff * Virtual pointer * Specification for memcpy * Move `page_table/cursor` out of legacy `aster_common` directory. * Moved `page_table/node` from legacy `aster_common` directory * Moved `page_table` from legacy `aster_common` * Moving cursor ownership stuff into `specs` * Ready to work on `cursor_steps` lemmas * Remove one lemma that shouldn't hold * Move owner/view files into specs directory * Migrate `frame` out of legacy `aster_common` * Eliminated `extern_const` declarations because we can just use consts now that `aster_common` is gone * Finished merging the legacy `aster_common` stuff over, some proofs did break in the process * Some proofs related to consts now need manual intervention; also fixed some consts that got changed somehow. * Revert "Some proofs related to consts now need manual intervention; also fixed some consts that got changed somehow." This reverts commit 82141a9. * Revert "Eliminated `extern_const` declarations because we can just use consts now that `aster_common` is gone" This reverts commit 5c0fa3d. Turns out `extern_const` is much easier to prove with even if it's not necessary. * merge * merge commits * minor tweaks * Move more proof definitions into `specs` * Admit some of the active proofs to push to public repo * Reconfigured `PageTableOwner` with new `TreeNodeView` implementation * CursorOwner changes * New structure for `move_forward` proof * Move `move_forward` work * stage * vmspace: tried experiment * Working on `map`, `unmap`, `split...` * Comment out manual trigger so `do_inc_index` will verify * Remove empty `aster_common` file * Remove the last trace of `aster_common`, yay! * Formatting * Cursor progress * Update vm to use `VirtPtr` * suppress warnings * fix some proofs * improve IO owner invariants and overlap specs * lemma for split * refine IO invariants and complete missing proofs * refine some API designs * prove `dispose_writer` * more proofs * Removing admits * Beginnings of memory model work * Move virtual pointer stuff to `virt_mem` in `ostd`, because it is really part of the ostd verification rather than a generic library * sync dv * fix broken proofs * verify `dispose_reader` * Use `NeverDrop` in place of `ManuallyDrop` * Starting on `Node::alloc` * refactor the tracked design * Getting guard_perm out of EntryOwner, phase 1 * Remove `guard_perm` from `EntryOwner` phase 2 * Finished removing `guard_perm` from `NodeOwner` and removing the extraneous `NodeEntryOwner` wrapper. * Re-verifying things that broke due to moving `guard_perm` * Reverifiying things that changed due to moving `guard_perm` * Reducing admits in cursor * Removing admits * More admits * More admits * Relate `pte` with `EntryOwner` (equivalent to how `Entry` is related * Structure of `split_if_mapped_huge` * Change `virt_mem_newer` to use separate frames * refine some ill-formed specs and proofs * Add the operations to manipulate the page table and TLB, assuming that the `GlobalMemView` is complete (no floating `MemView` objects) * update * `protect_next` uncommented * Some proofs and trigger updates * Working on virtual memory example; includes changes to `virt_mem_newer` * Example with mapping a page * Split up pre- and post-conditions of `map` for readability * Tweaking `map` doc example * Working on `guard_perm` assumptions. * update * revert toolchain * prove `activate_writer` * Assorted admits * `CursorView` updated for new specs * Working on some fiddling conditions about locked nodes * Fix breaking change in `layout` * Update dv * Relating page table nodes to their regions * Fix the performance issue by moving the branches of `map` out into their own functions. * Uniqueness of pt guards, stage 1: pt metadata carries correct path * Added predicate map over trees to deal with some challenging reasoning about all nodes * Added predicate map over trees * Working more on inline docs for `vmspace` specs, with hyperlinks to `page_table_cursor_specs.rs` * Big step toward using Set<Mapping> everywhere * Clearing admits * finish vm io * fix warnings and fmt * fix triggers * Admitpocalypse * Assorted fixes * `split_if_mapped_huge` * `query` using view spec * Fixed issue with the `map` top level proof. Resulted in adding some admits that will need to get fixed. * Page life cycle criteria for nodes * Mostly work on `jump` admits. * Add missing `res` * Finalize non-duplication theorem, but still need to figure out how best to present it * First stab at the top-level memory document * Version numbers in `Cargo.lock` * Top-level theorems: now with more TLB * Delete old `virt_mem.rs` * Simplifying `vm_space` specs * Documented `linked_list` * Fixed some lingering admits in `linked_list` * Working on `vm_space` documentation * Assorted fixes * More in-depth tlb modeling, for `unmap` * Beginning to separate out safety conditions from correctness * `UniqueFrame` documentation, shifting preconditions to separate safety from correctness * Working on docs and reorganizing `vm_space` * Finished `vm_space` documentation (at least for now) * Make `vm_space_specs` public and not re-exported, for cleaner docs. * Bullet points for multiple conditions in docs * Fixed `MetaSlot` vs. `MetaSlotStorage` abstraction issue. `MetaSlotStorage` can be modeled as a cell again! * `Repr` now supports underlying datatypes with their own permissions, so it's able to realistically apply to `MetaSlot`s now. * documentation and pretty * Constructing inner perms from meta perm * Documentation of `node/mod.rs` * Using the new ReprPtr more widely * Rename `NeverDrop` to `ManuallyDrop` and use it in all cases * Eliminated `dropped_slots` * Documented `meta` except the "drop" related functions * Done documenting `meta.rs` * Simplifying preconitions in `Frame` * prettier and triggers * `PCell` migration * documenting `vm_space` * documenting the lifecycle of vmspaces * Working on `Frame<M>` documentation * Finish `frame/mod.rs` documentation * Remove `vstd_extra::ManuallyDrop` and some duplicate imports * Remove duplicat imports --------- Co-authored-by: Hiroki <haobin.chen@certik.com>
1 parent bc16877 commit dddf63c

32 files changed

Lines changed: 1034 additions & 719 deletions

‎ostd/specs/mm/frame/frame_lifecycle.rs‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ use crate::mm::frame::meta::AnyFrameMeta;
44
use crate::mm::frame::Frame;
55
use crate::mm::Paddr;
66
use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;
7+
use crate::specs::mm::frame::frame_specs::*;
78

89
use vstd_extra::drop_tracking::*;
910

‎ostd/specs/mm/frame/frame_specs.rs‎

Lines changed: 79 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -3,28 +3,94 @@ use vstd::prelude::*;
33
use vstd_extra::cast_ptr::*;
44
use vstd_extra::ownership::*;
55

6-
use crate::mm::frame::meta::{mapping::frame_to_index, get_slot_spec, REF_COUNT_UNUSED};
6+
use crate::mm::frame::meta::{get_slot_spec, mapping::frame_to_index, REF_COUNT_UNUSED};
77
use crate::mm::frame::*;
88
use crate::mm::{Paddr, PagingLevel, Vaddr};
99
use crate::specs::arch::mm::{MAX_NR_PAGES, MAX_PADDR, PAGE_SIZE};
10-
use crate::specs::mm::frame::meta_owners::MetaSlotStorage;
10+
use crate::specs::mm::frame::meta_owners::{MetaSlotStorage, MetaPerm};
1111
use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;
1212

1313
use core::marker::PhantomData;
1414

1515
verus! {
1616

17-
impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> UniqueFrame<M> {
18-
19-
pub open spec fn from_unused_spec(paddr: Paddr, metadata: M, pre: MetaRegionOwners)
20-
-> Self
21-
recommends
22-
paddr % PAGE_SIZE == 0,
23-
paddr < MAX_PADDR,
24-
pre.inv(),
25-
{
26-
let ptr = get_slot_spec(paddr);
27-
UniqueFrame { ptr, _marker: PhantomData }
17+
impl<'a, M: AnyFrameMeta> Frame<M> {
18+
/// # Internal Safety Spec
19+
/// This is a condition that supports unsafe Rust encapsulation. It should never be exposed to
20+
/// the API client.
21+
pub open spec fn from_raw_requires(regions: MetaRegionOwners, paddr: Paddr) -> bool {
22+
&&& regions.slot_owners.contains_key(frame_to_index(paddr))
23+
&&& regions.slot_owners[frame_to_index(paddr)].raw_count == 1
24+
&&& regions.slot_owners[frame_to_index(paddr)].self_addr == frame_to_meta(paddr)
25+
&&& has_safe_slot(paddr) // TODO: this should actually imply the first condition
26+
&&& !regions.slots.contains_key(frame_to_index(paddr)) // Whomever called `into_raw` should hold the permission.
27+
&&& regions.inv()
28+
}
29+
30+
pub open spec fn from_raw_ensures(
31+
old_regions: MetaRegionOwners,
32+
new_regions: MetaRegionOwners,
33+
paddr: Paddr,
34+
r: Self,
35+
) -> bool {
36+
&&& new_regions.inv()
37+
&&& new_regions.slots.contains_key(frame_to_index(paddr))
38+
&&& new_regions.slot_owners[frame_to_index(paddr)].raw_count == 0
39+
&&& new_regions.slot_owners[frame_to_index(paddr)].inner_perms ==
40+
old_regions.slot_owners[frame_to_index(paddr)].inner_perms
41+
&&& new_regions.slot_owners[frame_to_index(paddr)].usage ==
42+
old_regions.slot_owners[frame_to_index(paddr)].usage
43+
&&& new_regions.slot_owners[frame_to_index(paddr)].path_if_in_pt ==
44+
old_regions.slot_owners[frame_to_index(paddr)].path_if_in_pt
45+
&&& new_regions.slot_owners[frame_to_index(paddr)].self_addr == r.ptr.addr()
46+
&&& forall|i: usize|
47+
#![trigger new_regions.slot_owners[i], old_regions.slot_owners[i]]
48+
i != frame_to_index(paddr) ==> new_regions.slot_owners[i] == old_regions.slot_owners[i]
49+
&&& r.ptr.addr() == frame_to_meta(paddr)
50+
&&& r.paddr() == paddr
51+
}
52+
53+
54+
// ── into_raw precondition predicates ──
55+
56+
/// **Safety Invariant**: The frame's structural invariant must hold.
57+
pub open spec fn into_raw_pre_frame_inv(self) -> bool {
58+
self.inv()
59+
}
60+
61+
/// **Bookkeeping**: The frame must be in use (not unused).
62+
pub open spec fn into_raw_pre_not_unused(self, regions: MetaRegionOwners) -> bool {
63+
regions.slot_owners[self.index()].inner_perms.ref_count.value() != REF_COUNT_UNUSED
64+
}
65+
66+
// ── into_raw postcondition predicates ──
67+
68+
/// **Correctness**: The frame's raw count is incremented.
69+
pub open spec fn into_raw_post_raw_count_incremented(
70+
self,
71+
old_regions: MetaRegionOwners,
72+
new_regions: MetaRegionOwners,
73+
) -> bool {
74+
&&& new_regions.slot_owners.contains_key(self.index())
75+
&&& new_regions.slot_owners[self.index()].raw_count
76+
== (old_regions.slot_owners[self.index()].raw_count + 1) as usize
77+
}
78+
79+
/// **Safety**: Frames other than this one are not affected by the call.
80+
pub open spec fn into_raw_post_noninterference(
81+
self,
82+
old_regions: MetaRegionOwners,
83+
new_regions: MetaRegionOwners,
84+
) -> bool {
85+
&&& forall|i: usize|
86+
#![trigger new_regions.slots[i], old_regions.slots[i]]
87+
i != self.index() && old_regions.slots.contains_key(i)
88+
==> new_regions.slots.contains_key(i)
89+
&& new_regions.slots[i] == old_regions.slots[i]
90+
&&& forall|i: usize|
91+
#![trigger new_regions.slot_owners[i], old_regions.slot_owners[i]]
92+
i != self.index() ==> new_regions.slot_owners[i] == old_regions.slot_owners[i]
93+
&&& new_regions.slot_owners.dom() =~= old_regions.slot_owners.dom()
2894
}
2995
}
3096

‎ostd/specs/mm/frame/linked_list/linked_list_owners.rs‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,12 @@
11
use vstd::atomic::*;
2+
use vstd::cell;
23
use vstd::prelude::*;
34
use vstd::seq_lib::*;
45
use vstd::simple_pptr::*;
5-
use vstd::cell;
66

7+
use vstd::std_specs::convert::FromSpecImpl;
78
use vstd_extra::cast_ptr::{Repr, ReprPtr};
89
use vstd_extra::ownership::*;
9-
use vstd::std_specs::convert::FromSpecImpl;
1010

1111
use core::marker::PhantomData;
1212

@@ -16,6 +16,7 @@ use crate::mm::Paddr;
1616
use crate::specs::arch::kspace::FRAME_METADATA_RANGE;
1717
use crate::specs::arch::mm::MAX_NR_PAGES;
1818
use crate::specs::mm::frame::mapping::META_SLOT_SIZE;
19+
use crate::specs::mm::frame::meta_owners::*;
1920
use crate::specs::mm::frame::unique::UniqueFrameOwner;
2021
use crate::specs::mm::frame::meta_owners::*;
2122

@@ -189,12 +190,12 @@ impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> LinkedListOwner<M> {
189190
&&& self.perms[i].value().metadata.prev is Some
190191
&&& self.perms[i].value().metadata.prev.unwrap().addr() == self.perms[i - 1].addr()
191192
&&& self.perms[i].value().metadata.prev.unwrap().ptr == self.perms[i - 1].points_to.pptr()
192-
}
193+
}
193194
&&& i < self.list.len() - 1 ==> {
194195
&&& self.perms[i].value().metadata.next is Some
195196
&&& self.perms[i].value().metadata.next.unwrap().addr() == self.perms[i + 1].addr()
196197
&&& self.perms[i].value().metadata.next.unwrap().ptr == self.perms[i + 1].points_to.pptr()
197-
}
198+
}
198199
&&& self.list[i].inv()
199200
&&& self.list[i].in_list == self.list_id
200201
}
@@ -534,7 +535,6 @@ impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> Repr<MetaSlot> for MetadataAsLink<M>
534535
uninterp spec fn wf(r: MetaSlot, perm: MetadataInnerPerms) -> bool;
535536

536537
uninterp spec fn to_repr_spec(self, perm: MetadataInnerPerms) -> (MetaSlot, MetadataInnerPerms);
537-
538538
#[verifier::external_body]
539539
fn to_repr(self, Tracked(perm): Tracked<&mut MetadataInnerPerms>) -> MetaSlot {
540540
unimplemented!()

‎ostd/specs/mm/frame/meta_owners.rs‎

Lines changed: 44 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33
//! - The invariants for both MetaSlot and MetaSlotModel.
44
//! - The primitives for MetaSlot.
55
use vstd::atomic::*;
6-
use vstd::cell::{self, PCell, PointsTo};
6+
use vstd::cell::pcell_maybe_uninit;
77
use vstd::prelude::*;
88
use vstd::simple_pptr::*;
99

@@ -12,15 +12,13 @@ use vstd_extra::ghost_tree::TreePath;
1212
use vstd_extra::ownership::*;
1313

1414
use super::*;
15-
use crate::mm::PagingLevel;
1615
use crate::mm::frame::meta::MetaSlot;
17-
use crate::specs::mm::frame::linked_list::linked_list_owners::StoredLink;
16+
use crate::mm::frame::AnyFrameMeta;
17+
use crate::mm::PagingLevel;
1818
use crate::specs::arch::kspace::FRAME_METADATA_RANGE;
1919
use crate::specs::arch::mm::NR_ENTRIES;
20+
use crate::specs::mm::frame::linked_list::linked_list_owners::StoredLink;
2021
use crate::specs::mm::frame::mapping::META_SLOT_SIZE;
21-
use crate::mm::frame::AnyFrameMeta;
22-
23-
use core::marker::PhantomData;
2422

2523
verus! {
2624

@@ -97,8 +95,8 @@ pub const REF_COUNT_UNIQUE: u64 = u64::MAX - 1;
9795
pub const REF_COUNT_MAX: u64 = i64::MAX as u64;
9896

9997
pub struct StoredPageTablePageMeta {
100-
pub nr_children: PCell<u16>,
101-
pub stray: PCell<bool>,
98+
pub nr_children: pcell_maybe_uninit::PCell<u16>,
99+
pub stray: pcell_maybe_uninit::PCell<bool>,
102100
pub level: PagingLevel,
103101
pub lock: PAtomicU8,
104102
}
@@ -192,15 +190,14 @@ impl MetaSlotStorage {
192190
}
193191

194192
pub tracked struct MetadataInnerPerms {
195-
pub storage: cell::PointsTo<MetaSlotStorage>,
193+
pub storage: pcell_maybe_uninit::PointsTo<MetaSlotStorage>,
196194
pub ref_count: PermissionU64,
197195
pub vtable_ptr: vstd::simple_pptr::PointsTo<usize>,
198196
pub in_list: PermissionU64,
199197
}
200198

201199
pub tracked struct MetaSlotOwner {
202-
/// The inner permissions of the metadata slot. When the slot is in use, these will be transferred to its current owner.
203-
pub inner_perms: Option<MetadataInnerPerms>,
200+
pub inner_perms: MetadataInnerPerms,
204201
pub self_addr: usize,
205202
pub usage: PageUsage,
206203
pub raw_count: usize,
@@ -209,26 +206,24 @@ pub tracked struct MetaSlotOwner {
209206

210207
impl Inv for MetaSlotOwner {
211208
open spec fn inv(self) -> bool {
212-
&&& self.inner_perms.unwrap().ref_count.value() == REF_COUNT_UNUSED ==> {
213-
/// An unused slot had better not have any raw pointer hanging around.
209+
&&& self.inner_perms.ref_count.value() == REF_COUNT_UNUSED ==> {
214210
&&& self.raw_count == 0
215-
&&& self.inner_perms is Some
216-
&&& self.inner_perms.unwrap().storage.is_uninit()
217-
&&& self.inner_perms.unwrap().vtable_ptr.is_uninit()
218-
&&& self.inner_perms.unwrap().in_list.value() == 0
211+
&&& self.inner_perms.storage.is_uninit()
212+
&&& self.inner_perms.vtable_ptr.is_uninit()
213+
&&& self.inner_perms.in_list.value() == 0
219214
}
220-
&&& self.inner_perms.unwrap().ref_count.value() == REF_COUNT_UNIQUE ==> {
221-
&&& self.inner_perms.unwrap().vtable_ptr.is_init()
215+
&&& self.inner_perms.ref_count.value() == REF_COUNT_UNIQUE ==> {
216+
&&& self.inner_perms.vtable_ptr.is_init()
217+
&&& self.inner_perms.storage.is_init()
218+
&&& self.inner_perms.in_list.value() == 0
222219
}
223-
&&& 0 < self.inner_perms.unwrap().ref_count.value() <= REF_COUNT_MAX ==> {
224-
&&& self.inner_perms.unwrap().vtable_ptr.is_init()
220+
&&& 0 < self.inner_perms.ref_count.value() <= REF_COUNT_MAX ==> {
221+
&&& self.inner_perms.vtable_ptr.is_init()
225222
}
226-
&&& REF_COUNT_MAX <= self.inner_perms.unwrap().ref_count.value() < REF_COUNT_UNUSED ==> { false }
227-
&&& self.inner_perms.unwrap().ref_count.value() == 0 ==> {
228-
// If we ever have 0 ref count, there had better be a `ManuallyDrop` somewhere keeping us from getting garbage collected.
229-
&&& self.raw_count > 0
230-
&&& self.inner_perms.unwrap().vtable_ptr.is_uninit()
231-
&&& self.inner_perms.unwrap().in_list.value() == 0
223+
&&& REF_COUNT_MAX <= self.inner_perms.ref_count.value() < REF_COUNT_UNIQUE ==> { false }
224+
&&& self.inner_perms.ref_count.value() == 0 ==> {
225+
&&& self.inner_perms.vtable_ptr.is_uninit()
226+
&&& self.inner_perms.in_list.value() == 0
232227
}
233228
&&& FRAME_METADATA_RANGE.start <= self.self_addr < FRAME_METADATA_RANGE.end
234229
&&& self.self_addr % META_SLOT_SIZE == 0
@@ -267,10 +262,10 @@ impl View for MetaSlotOwner {
267262
type V = MetaSlotModel;
268263

269264
open spec fn view(&self) -> Self::V {
270-
let storage = self.inner_perms.unwrap().storage.mem_contents();
271-
let ref_count = self.inner_perms.unwrap().ref_count.value();
272-
let vtable_ptr = self.inner_perms.unwrap().vtable_ptr.mem_contents();
273-
let in_list = self.inner_perms.unwrap().in_list.value();
265+
let storage = self.inner_perms.storage.mem_contents();
266+
let ref_count = self.inner_perms.ref_count.value();
267+
let vtable_ptr = self.inner_perms.vtable_ptr.mem_contents();
268+
let in_list = self.inner_perms.in_list.value();
274269
let self_addr = self.self_addr;
275270
let usage = self.usage;
276271
let status = match ref_count {
@@ -293,18 +288,30 @@ impl OwnerOf for MetaSlot {
293288
type Owner = MetaSlotOwner;
294289

295290
open spec fn wf(self, owner: Self::Owner) -> bool {
296-
&&& owner.inner_perms is Some
297-
&&& self.storage.id() == owner.inner_perms.unwrap().storage.id()
298-
&&& self.ref_count.id() == owner.inner_perms.unwrap().ref_count.id()
299-
&&& self.vtable_ptr == owner.inner_perms.unwrap().vtable_ptr.pptr()
300-
&&& self.in_list.id() == owner.inner_perms.unwrap().in_list.id()
291+
&&& self.storage.id() == owner.inner_perms.storage.id()
292+
&&& self.ref_count.id() == owner.inner_perms.ref_count.id()
293+
&&& self.vtable_ptr == owner.inner_perms.vtable_ptr.pptr()
294+
&&& self.in_list.id() == owner.inner_perms.in_list.id()
301295
}
302296
}
303297

304298
impl ModelOf for MetaSlot {
305299

306300
}
307301

302+
impl MetaSlotOwner {
303+
pub axiom fn take_inner_perms(tracked &mut self) -> (tracked res: MetadataInnerPerms)
304+
ensures
305+
res == old(self).inner_perms,
306+
self.self_addr == old(self).self_addr,
307+
self.usage == old(self).usage,
308+
self.raw_count == old(self).raw_count,
309+
self.path_if_in_pt == old(self).path_if_in_pt;
310+
311+
pub axiom fn sync_inner(tracked &mut self, inner_perms: &MetadataInnerPerms)
312+
ensures *self == (Self { inner_perms: *inner_perms, ..*old(self) });
313+
}
314+
308315
pub struct Metadata<M: AnyFrameMeta> {
309316
pub metadata: M,
310317
pub ref_count: u64,
@@ -316,7 +323,7 @@ impl<M: AnyFrameMeta + Repr<MetaSlotStorage>> Metadata<M> {
316323
/// The metadata value is an abstract function of the inner permissions,
317324
/// since extracting `M` from `MetaSlotStorage` requires `M::Perm` which
318325
/// is not stored in `MetadataInnerPerms`.
319-
pub uninterp spec fn metadata_from_inner_perms(perm: cell::PointsTo<MetaSlotStorage>) -> M;
326+
pub uninterp spec fn metadata_from_inner_perms(perm: pcell_maybe_uninit::PointsTo<MetaSlotStorage>) -> M;
320327
}
321328

322329
impl<M: AnyFrameMeta + Repr<MetaSlotStorage>> Repr<MetaSlot> for Metadata<M> {

‎ostd/specs/mm/frame/meta_region_owners.rs‎

Lines changed: 31 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -5,14 +5,15 @@ use vstd::simple_pptr::{self, *};
55

66
use core::ops::Range;
77

8+
use vstd_extra::cast_ptr::Repr;
89
use vstd_extra::ghost_tree::TreePath;
910
use vstd_extra::ownership::*;
1011

11-
use super::meta_owners::{MetaSlotModel, MetaSlotOwner};
12+
use super::meta_owners::{MetaPerm, MetaSlotModel, MetaSlotOwner, MetaSlotStorage};
1213
use super::*;
1314
use crate::mm::frame::meta::{
1415
mapping::{frame_to_index_spec, frame_to_meta, max_meta_slots, meta_addr, META_SLOT_SIZE},
15-
MetaSlot,
16+
AnyFrameMeta, MetaSlot,
1617
};
1718
use crate::mm::Paddr;
1819
use crate::specs::arch::kspace::FRAME_METADATA_RANGE;
@@ -66,13 +67,19 @@ impl Inv for MetaRegionOwners {
6667
self.slots.contains_key(i) ==> {
6768
&&& self.slot_owners.contains_key(i)
6869
&&& self.slot_owners[i].inv()
69-
&&& self.slot_owners[i].inner_perms is Some
7070
&&& self.slots[i].is_init()
7171
&&& self.slots[i].addr() == meta_addr(i)
7272
&&& self.slots[i].value().wf(self.slot_owners[i])
73+
&&& self.slot_owners.contains_key(i)
7374
&&& self.slot_owners[i].self_addr == self.slots[i].addr()
7475
}
7576
}
77+
&&& {
78+
forall|i: usize| #[trigger]
79+
self.slot_owners.contains_key(i) ==> {
80+
&&& self.slot_owners[i].inv()
81+
}
82+
}
7683
}
7784
}
7885

@@ -115,9 +122,8 @@ impl MetaRegionOwners {
115122
recommends
116123
self.inv(),
117124
i < max_meta_slots() as usize,
118-
self.slot_owners[i].inner_perms is Some,
119125
{
120-
self.slot_owners[i].inner_perms.unwrap().ref_count.value()
126+
self.slot_owners[i].inner_perms.ref_count.value()
121127
}
122128

123129
pub open spec fn paddr_range_in_region(self, range: Range<Paddr>) -> bool
@@ -163,6 +169,26 @@ impl MetaRegionOwners {
163169
{
164170
assert((frame_to_index_spec(paddr)) < max_meta_slots() as usize);
165171
}
172+
173+
pub axiom fn sync_perm<M: AnyFrameMeta + Repr<MetaSlotStorage>>(
174+
tracked &mut self,
175+
index: usize,
176+
perm: &MetaPerm<M>,
177+
)
178+
ensures
179+
self.slots == old(self).slots.insert(index, perm.points_to),
180+
self.slot_owners == old(self).slot_owners;
181+
182+
pub axiom fn copy_perm<M: AnyFrameMeta + Repr<MetaSlotStorage>>(
183+
tracked &mut self,
184+
index: usize,
185+
) -> (tracked perm: MetaPerm<M>)
186+
requires
187+
old(self).slots.contains_key(index),
188+
ensures
189+
perm.points_to == old(self).slots[index],
190+
self.slots == old(self).slots.remove(index),
191+
self.slot_owners == old(self).slot_owners;
166192
}
167193

168194
} // verus!

0 commit comments

Comments
 (0)