performance

.github/workflows/ci-irc11.yml

@@ -49,7 +49,7 @@ jobs:
     env:
       CARGO_TERM_COLOR: always
       VERUS_REPOSITORY: https://github.com/asterinas/verus.git
-      VERUS_BASE_COMMIT: 2ceabf8168c994d61995ce860e0d8b7cab0f9c1b
+      VERUS_BASE_COMMIT: 38f659b0e97a003d4fed73e083c71e786c6a3523
       VERUS_IRC11_PATCH: tools/patches/verus-irc11.patch
       VERUS_COMPAT_PATCH: tools/patches/verus-irc11-vstd.patch
 

ostd/specs/mm/embedding/list_store.rs

@@ -744,7 +744,9 @@ impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> ListStore<M> {
         let tracked empty = tracked_empty_list_owner::<M>();
         self.lists.tracked_insert(id, empty);
         assert(self.lists[id].list.len() == 0);
-        assert(self.lists[id].relate_region(self.regions));
+        assert(self.lists[id].relate_region(self.regions)) by {
+            reveal(LinkedListOwner::relate_region);
+        };
         assert(self.cursors == old_self.cursors);
         assert(self.lists.dom().disjoint(self.cursors.dom()));
         assert(self.lists[id].list_id == 0);
@@ -767,14 +769,16 @@ impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> ListStore<M> {
         let ghost dropped_id = self.lists[id].list_id;
         let ghost is_empty = self.lists[id].list.len() == 0;
         assert(self.lists[id].relate_region(self.regions));
+        self.lists[id].lemma_relate_region_shape(self.regions);
         assert forall|i: int|
             #![trigger meta_to_index(self.lists[id].list[i].paddr)]
             0 <= i < self.lists[id].list.len() implies self.regions.slot_owners[meta_to_index(
             self.lists[id].list[i].paddr,
         )].paths_in_pt.is_empty() by {
             let idx = meta_to_index(self.lists[id].list[i].paddr);
             let _ = self.lists[id].list[i];
-            self.lists[id].relate_region_at_facts(self.regions, i);
+            self.lists[id].lemma_relate_region_at_index(self.regions, i);
+            self.lists[id].lemma_relate_region_at_facts(self.regions, i);
             assert(self.regions.contains(idx));
             assert(self.regions.ref_count(idx) == REF_COUNT_UNIQUE);
             assert(self.regions.slot_owners[idx].usage is Frame);

ostd/specs/mm/embedding/mod.rs

@@ -52,7 +52,10 @@ use crate::specs::{
             meta_region_owners::MetaRegionOwners,
         },
         io::VmIoOwner,
-        page_table::{cursor::owners::CursorOwner, node::Guards},
+        page_table::{
+            cursor::owners::{CursorContinuation, CursorOwner},
+            node::Guards,
+        },
         tlb::TlbModel,
     },
 };
@@ -2448,8 +2451,6 @@ proof fn lemma_step_segment_drop<'rcu>(tracked s: &mut VmStore<'rcu>, sid: Segme
     ensures
         final(s).inv(),
 {
-    reveal(VmStore::structural_inv);
-    reveal(VmStore::accounting_inv);
     let ghost s_before = *s;
     let ghost old_regions = s.regions;
     let ghost old_frames = s.frames;
@@ -2482,7 +2483,7 @@ proof fn lemma_step_segment_drop<'rcu>(tracked s: &mut VmStore<'rcu>, sid: Segme
         s.segments,
         index_to_frame(idx),
     ) == 0 by {
-        reveal(VmStore::accounting_inv);
+        lemma_accounting_inv_at(s_before, idx);
         let paddr = index_to_frame(idx);
         assert(paddr == (idx * PAGE_SIZE) as usize);
         assert(paddr % PAGE_SIZE == 0);
@@ -2508,7 +2509,7 @@ proof fn lemma_step_segment_drop<'rcu>(tracked s: &mut VmStore<'rcu>, sid: Segme
         s.segments,
         index_to_frame(idx),
     ) > 0 by {
-        reveal(VmStore::accounting_inv);
+        lemma_accounting_inv_at(s_before, idx);
         let paddr = index_to_frame(idx);
         assert(paddr == (idx * PAGE_SIZE) as usize);
         assert(paddr % PAGE_SIZE == 0);
@@ -2540,7 +2541,7 @@ proof fn lemma_step_segment_drop<'rcu>(tracked s: &mut VmStore<'rcu>, sid: Segme
             index_to_frame(idx),
         )
     } by {
-        reveal(VmStore::accounting_inv);
+        lemma_accounting_inv_at(s_before, idx);
         let paddr = index_to_frame(idx);
         assert(paddr == (idx * PAGE_SIZE) as usize);
         assert(paddr % PAGE_SIZE == 0);
@@ -2580,10 +2581,10 @@ proof fn lemma_step_segment_drop<'rcu>(tracked s: &mut VmStore<'rcu>, sid: Segme
         s.frames.contains_key(fid_other) implies s.regions.slot_owner(
         s.frames[fid_other].paddr,
     ).usage is Frame by {
-        reveal(VmStore::structural_inv);
-        reveal(VmStore::accounting_inv);
         let other_idx = frame_to_index(s.frames[fid_other].paddr);
         let other_paddr = index_to_frame(other_idx);
+        lemma_structural_inv_frame(s_before, fid_other);
+        lemma_accounting_inv_at(s_before, other_idx);
         assert(old_regions.slot_owners[other_idx].usage is Frame);
         assert(old_frames.dom().filter(
             |gid: FrameId| frame_to_index(old_frames[gid].paddr) == other_idx,
@@ -2602,11 +2603,11 @@ proof fn lemma_step_segment_drop<'rcu>(tracked s: &mut VmStore<'rcu>, sid: Segme
         s.segments.contains_key(sid_other) && s.segments[sid_other].range.start <= paddr_c
             < s.segments[sid_other].range.end && paddr_c % PAGE_SIZE
             == 0 implies s.regions.slot_owner(paddr_c).usage is Frame by {
-        reveal(VmStore::structural_inv);
         let cov_idx = frame_to_index(paddr_c);
         assert(sid_other != sid);
         assert(old_segments.contains_key(sid_other));
         assert(old_segments[sid_other] == s.segments[sid_other]);
+        lemma_structural_inv_segment(s_before, sid_other, paddr_c);
         assert(old_regions.slot_owners[cov_idx].usage is Frame);
     };
     assert forall|u: UniqueId| #[trigger] s.unique_frames.contains_key(u) implies {
@@ -2616,11 +2617,10 @@ proof fn lemma_step_segment_drop<'rcu>(tracked s: &mut VmStore<'rcu>, sid: Segme
         &&& so.in_list_perm.value() == 0
         &&& so.paths_in_pt.is_empty()
     } by {
-        reveal(VmStore::structural_inv);
-        reveal(VmStore::accounting_inv);
         let u_paddr = s.unique_frames[u].paddr;
         let u_idx = frame_to_index(u_paddr);
         assert(old(s).unique_frames.contains_key(u));
+        reveal(VmStore::structural_inv);
         assert(valid_frame_paddr(u_paddr));
         s.regions.lemma_contains_valid_frame_paddr(u_paddr);
         // Old UNIQUE validity at `u`.
@@ -2919,6 +2919,8 @@ proof fn lemma_step_segment_next<'rcu>(tracked s: &mut VmStore<'rcu>, sid: Segme
         &&& so.in_list_perm.value() == 0
         &&& so.paths_in_pt.is_empty()
     } by {};
+    reveal(CursorContinuation::map_children);
+    reveal(CursorOwner::path_metaregion_sound);
 }
 
 #[verifier::spinoff_prover]