Merge branch 'phaseII/verified' into mutexspec

Author: rikosellic

aster_common/src/arch/mod.rs

@@ -2,4 +2,4 @@ mod x86_64;
 
 pub use x86_64::*;
 
-use super::*;
+use super::*;

aster_common/src/lib.rs

@@ -1,3 +1,7 @@
+#![allow(non_snake_case)]
+#![allow(non_camel_case_types)]
+#![allow(unused_attributes)]
+
 mod arch;
 mod mm;
 mod task;

aster_common/src/mm/frame/linked_list.rs

@@ -240,7 +240,7 @@ impl<M: AnyFrameMeta + Repr<MetaSlotInner>> AnyFrameMeta for Link<M> {
         false
     }
 
-    spec fn vtable_ptr(&self) -> usize;
+    uninterp spec fn vtable_ptr(&self) -> usize;
 }
 
 } // verus!

aster_common/src/mm/frame/linked_list_owners.rs

@@ -14,7 +14,7 @@ pub ghost struct LinkModel {
 }
 
 impl Inv for LinkModel {
-    open spec fn inv(&self) -> bool {
+    open spec fn inv(self) -> bool {
         true
     }
 }
@@ -25,26 +25,26 @@ pub tracked struct LinkOwner {
 }
 
 impl Inv for LinkOwner {
-    open spec fn inv(&self) -> bool {
+    open spec fn inv(self) -> bool {
         true
     }
 }
 
 impl InvView for LinkOwner {
     type V = LinkModel;
 
-    open spec fn view(&self) -> Self::V {
+    open spec fn view(self) -> Self::V {
         LinkModel { paddr: self.paddr }
     }
 
-    proof fn view_preserves_inv(&self) {
+    proof fn view_preserves_inv(self) {
     }
 }
 
 impl<M: AnyFrameMeta + Repr<MetaSlotInner>> OwnerOf for Link<M> {
     type Owner = LinkOwner;
 
-    open spec fn wf(&self, owner: &Self::Owner) -> bool {
+    open spec fn wf(self, owner: Self::Owner) -> bool {
         true
         //        &&& owner.self_perm@.mem_contents().value() == self
         //        &&& owner.next == self.next
@@ -80,7 +80,7 @@ impl LinkedListModel {
 }
 
 impl Inv for LinkedListModel {
-    open spec fn inv(&self) -> bool {
+    open spec fn inv(self) -> bool {
         true
     }
 }
@@ -93,7 +93,7 @@ pub tracked struct LinkedListOwner<M: AnyFrameMeta + Repr<MetaSlotInner>> {
 }
 
 impl<M: AnyFrameMeta + Repr<MetaSlotInner>> Inv for LinkedListOwner<M> {
-    open spec fn inv(&self) -> bool {
+    open spec fn inv(self) -> bool {
         forall|i: int| 0 <= i < self.list.len() ==> self.inv_at(i)
     }
 }
@@ -108,7 +108,7 @@ impl<M: AnyFrameMeta + Repr<MetaSlotInner>> LinkedListOwner<M> {
         &&& FRAME_METADATA_RANGE().start <= self.perms[i]@.addr() < FRAME_METADATA_RANGE().start
             + MAX_NR_PAGES() * META_SLOT_SIZE()
         &&& self.perms[i]@.is_init()
-        &&& self.perms[i]@.value().wf(&self.list[i])
+        &&& self.perms[i]@.value().wf(self.list[i])
         &&& i == 0 <==> self.perms[i]@.mem_contents().value().prev is None
         &&& i == self.list.len() - 1 <==> self.perms[i]@.value().next is None
         &&& 0 < i ==> self.perms[i]@.value().prev is Some && self.perms[i]@.value().prev.unwrap()
@@ -144,11 +144,11 @@ impl<M: AnyFrameMeta + Repr<MetaSlotInner>> LinkedListOwner<M> {
 impl<M: AnyFrameMeta + Repr<MetaSlotInner>> InvView for LinkedListOwner<M> {
     type V = LinkedListModel;
 
-    open spec fn view(&self) -> Self::V {
+    open spec fn view(self) -> Self::V {
         LinkedListModel { list: Self::view_helper(self.list) }
     }
 
-    proof fn view_preserves_inv(&self) {
+    proof fn view_preserves_inv(self) {
     }
 }
 
@@ -174,7 +174,7 @@ impl<M: AnyFrameMeta + Repr<MetaSlotInner>> LinkedListOwner<M> {
 impl<M: AnyFrameMeta + Repr<MetaSlotInner>> OwnerOf for LinkedList<M> {
     type Owner = LinkedListOwner<M>;
 
-    open spec fn wf(&self, owner: &Self::Owner) -> bool {
+    open spec fn wf(self, owner: Self::Owner) -> bool {
         &&& self.front is None <==> owner.list.len() == 0
         &&& self.back is None <==> owner.list.len() == 0
         &&& owner.list.len() > 0 ==> self.front is Some && self.front.unwrap().addr()
@@ -198,7 +198,7 @@ pub ghost struct CursorModel {
 }
 
 impl Inv for CursorModel {
-    open spec fn inv(&self) -> bool {
+    open spec fn inv(self) -> bool {
         self.list_model.inv()
     }
 }
@@ -211,7 +211,7 @@ pub tracked struct CursorOwner<M: AnyFrameMeta + Repr<MetaSlotInner>> {
 }
 
 impl<M: AnyFrameMeta + Repr<MetaSlotInner>> Inv for CursorOwner<M> {
-    open spec fn inv(&self) -> bool {
+    open spec fn inv(self) -> bool {
         &&& 0 <= self.index <= self.length()
         &&& self.list_own.inv()
     }
@@ -220,7 +220,7 @@ impl<M: AnyFrameMeta + Repr<MetaSlotInner>> Inv for CursorOwner<M> {
 impl<M: AnyFrameMeta + Repr<MetaSlotInner>> InvView for CursorOwner<M> {
     type V = CursorModel;
 
-    open spec fn view(&self) -> Self::V {
+    open spec fn view(self) -> Self::V {
         let list = self.list_own.view();
         CursorModel {
             fore: list.list.take(self.index),
@@ -229,21 +229,21 @@ impl<M: AnyFrameMeta + Repr<MetaSlotInner>> InvView for CursorOwner<M> {
         }
     }
 
-    proof fn view_preserves_inv(&self) {
+    proof fn view_preserves_inv(self) {
     }
 }
 
 impl<M: AnyFrameMeta + Repr<MetaSlotInner>> OwnerOf for CursorMut<M> {
     type Owner = CursorOwner<M>;
 
-    open spec fn wf(&self, owner: &Self::Owner) -> bool {
+    open spec fn wf(self, owner: Self::Owner) -> bool {
         &&& 0 <= owner.index < owner.length() ==> self.current.is_some()
             && self.current.unwrap().addr() == owner.list_own.list[owner.index].paddr
             && owner.list_own.perms[owner.index]@.pptr() == self.current.unwrap()
         &&& owner.index == owner.list_own.list.len() ==> self.current.is_none()
         &&& owner.list_perm@.pptr() == self.list
         &&& owner.list_perm@.is_init()
-        &&& owner.list_perm@.mem_contents().value().wf(&owner.list_own)
+        &&& owner.list_perm@.mem_contents().value().wf(owner.list_own)
     }
 }
 

aster_common/src/mm/frame/meta.rs

@@ -139,7 +139,7 @@ impl MetaSlot {
         Tracked(owner): Tracked<&MetaSlotOwner>,
     ) -> (res: ReprPtr<MetaSlotStorage, T>)
         requires
-            self.wf(owner),
+            self.wf(*owner),
             owner.inv(),
             addr == owner.storage@.addr(),
         ensures

aster_common/src/mm/frame/meta_owners.rs

@@ -103,7 +103,7 @@ pub tracked struct MetaSlotOwner {
 }
 
 impl Inv for MetaSlotOwner {
-    open spec fn inv(&self) -> bool {
+    open spec fn inv(self) -> bool {
         &&& self.ref_count@.value() == REF_COUNT_UNUSED ==> {
             &&& self.vtable_ptr@.is_uninit()
             &&& self.in_list@.value() == 0
@@ -135,7 +135,7 @@ pub ghost struct MetaSlotModel {
 }
 
 impl Inv for MetaSlotModel {
-    open spec fn inv(&self) -> bool {
+    open spec fn inv(self) -> bool {
         match self.ref_count {
             REF_COUNT_UNUSED => {
                 &&& self.vtable_ptr.is_uninit()
@@ -155,7 +155,7 @@ impl Inv for MetaSlotModel {
 impl InvView for MetaSlotOwner {
     type V = MetaSlotModel;
 
-    open spec fn view(&self) -> Self::V {
+    open spec fn view(self) -> Self::V {
         let storage = self.storage@.mem_contents();
         let ref_count = self.ref_count@.value();
         let vtable_ptr = self.vtable_ptr@.mem_contents();
@@ -172,15 +172,15 @@ impl InvView for MetaSlotOwner {
         MetaSlotModel { status, storage, ref_count, vtable_ptr, in_list, self_addr, usage }
     }
 
-    proof fn view_preserves_inv(&self) {
+    proof fn view_preserves_inv(self) {
         admit()
     }
 }
 
 impl OwnerOf for MetaSlot {
     type Owner = MetaSlotOwner;
 
-    open spec fn wf(&self, owner: &Self::Owner) -> bool {
+    open spec fn wf(self, owner: Self::Owner) -> bool {
         &&& self.storage == owner.storage@.pptr()
         &&& self.ref_count.id() == owner.ref_count@.id()
         &&& self.vtable_ptr == owner.vtable_ptr@.pptr()

aster_common/src/mm/frame/meta_region_owners.rs

@@ -24,7 +24,7 @@ pub ghost struct MetaRegionModel {
 }
 
 impl Inv for MetaRegionOwners {
-    open spec fn inv(&self) -> bool {
+    open spec fn inv(self) -> bool {
         &&& self.slots.dom().finite()
         &&& {
             // All accessible slots are within the valid address range.
@@ -44,7 +44,7 @@ impl Inv for MetaRegionOwners {
                 self.slots.contains_key(i) ==> {
                     &&& self.slots[i]@.is_init()
                     &&& self.slots[i]@.addr() == meta_addr(i)
-                    &&& self.slots[i]@.value().wf(&self.slot_owners[i])
+                    &&& self.slots[i]@.value().wf(self.slot_owners[i])
                     &&& self.slot_owners[i].self_addr == self.slots[i]@.addr()
                     &&& !self.dropped_slots.contains_key(i)
                 }
@@ -54,7 +54,7 @@ impl Inv for MetaRegionOwners {
                 self.dropped_slots.contains_key(i) ==> {
                     &&& self.dropped_slots[i]@.is_init()
                     &&& self.dropped_slots[i]@.addr() == meta_addr(i)
-                    &&& self.dropped_slots[i]@.value().wf(&self.slot_owners[i])
+                    &&& self.dropped_slots[i]@.value().wf(self.slot_owners[i])
                     &&& self.slot_owners[i].self_addr == self.dropped_slots[i]@.addr()
                     &&& !self.slots.contains_key(i)
                 }
@@ -63,7 +63,7 @@ impl Inv for MetaRegionOwners {
 }
 
 impl Inv for MetaRegionModel {
-    open spec fn inv(&self) -> bool {
+    open spec fn inv(self) -> bool {
         &&& self.slots.dom().finite()
         &&& forall|i: usize| i < max_meta_slots() <==> #[trigger] self.slots.contains_key(i)
         &&& forall|i: usize| #[trigger] self.slots.contains_key(i) ==> self.slots[i].inv()
@@ -73,19 +73,19 @@ impl Inv for MetaRegionModel {
 impl InvView for MetaRegionOwners {
     type V = MetaRegionModel;
 
-    open spec fn view(&self) -> Self::V {
+    open spec fn view(self) -> Self::V {
         let slots = self.slot_owners.map_values(|s: MetaSlotOwner| s.view());
         MetaRegionModel { slots }
     }
 
     // XXX: verus `map_values` does not preserves the `finite()` attribute.
-    axiom fn view_preserves_inv(&self);
+    axiom fn view_preserves_inv(self);
 }
 
 impl OwnerOf for MetaRegion {
     type Owner = MetaRegionOwners;
 
-    open spec fn wf(&self, owner: &Self::Owner) -> bool {
+    open spec fn wf(self, owner: Self::Owner) -> bool {
         true
     }
 }

aster_common/src/mm/frame/mod.rs

@@ -41,7 +41,7 @@ pub struct Frame<M: AnyFrameMeta> {
 }
 
 impl<M: AnyFrameMeta> Inv for Frame<M> {
-    open spec fn inv(&self) -> bool {
+    open spec fn inv(self) -> bool {
         &&& self.ptr.addr() % META_SLOT_SIZE() == 0
         &&& FRAME_METADATA_RANGE().start <= self.ptr.addr() < FRAME_METADATA_RANGE().start
             + MAX_NR_PAGES() * META_SLOT_SIZE()
@@ -65,12 +65,12 @@ impl<M: AnyFrameMeta> Frame<M> {
         owner:
             MetaSlotOwner,
         //        Tracked(p_inner): Tracked<&'a cell::PointsTo<MetaSlotInner>>,
-    ) -> (res: &PageTablePageMeta<C>)
+    ) -> (res: &'a PageTablePageMeta<C>)
         requires
             self.inv(),
             p_slot.pptr() == self.ptr,
             p_slot.is_init(),
-            p_slot.value().wf(&owner),
+            p_slot.value().wf(owner),
             is_variant(owner.view().storage.value(), "PTNode"),
         ensures
     //            PTNode(*res) == owner.view().storage.value(),

aster_common/src/mm/frame/unique.rs

@@ -24,7 +24,7 @@ pub ghost struct UniqueFrameModel<M: AnyFrameMeta + Repr<MetaSlotStorage> + Owne
 }
 
 impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> Inv for UniqueFrameOwner<M> {
-    open spec fn inv(&self) -> bool {
+    open spec fn inv(self) -> bool {
         &&& self.meta_perm@.is_init()
         &&& self.meta_perm@.wf()
         &&& self.slot_index == frame_to_index(meta_to_frame(self.meta_perm@.addr()))
@@ -36,30 +36,30 @@ impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> Inv for UniqueFrameOwner
 }
 
 impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> Inv for UniqueFrameModel<M> {
-    open spec fn inv(&self) -> bool {
+    open spec fn inv(self) -> bool {
         true
     }
 }
 
 impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> InvView for UniqueFrameOwner<M> {
     type V = UniqueFrameModel<M>;
 
-    open spec fn view(&self) -> Self::V {
+    open spec fn view(self) -> Self::V {
         UniqueFrameModel { meta: self.meta_own@@ }
     }
 
-    proof fn view_preserves_inv(&self) {
+    proof fn view_preserves_inv(self) {
     }
 }
 
 impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> UniqueFrameOwner<M> {
-    pub open spec fn perm_inv(&self, perm: PointsTo<MetaSlot>) -> bool {
+    pub open spec fn perm_inv(self, perm: PointsTo<MetaSlot>) -> bool {
         &&& perm.is_init()
         &&& perm.value().storage.addr() == self.meta_perm@.addr()
         &&& perm.value().storage.addr() == self.meta_perm@.points_to@.addr()
     }
 
-    pub open spec fn global_inv(&self, regions: MetaRegionOwners) -> bool {
+    pub open spec fn global_inv(self, regions: MetaRegionOwners) -> bool {
         &&& regions.slots.contains_key(self.slot_index) ==> self.perm_inv(
             regions.slots[self.slot_index]@,
         )
@@ -72,7 +72,7 @@ impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> UniqueFrameOwner<M> {
 impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> OwnerOf for UniqueFrame<M> {
     type Owner = UniqueFrameOwner<M>;
 
-    open spec fn wf(&self, owner: &Self::Owner) -> bool {
+    open spec fn wf(self, owner: Self::Owner) -> bool {
         &&& self.ptr.addr() == owner.meta_perm@.addr()
     }
 }