Experiment: verification for dma module

ostd/specs/mm/frame/frame_lifecycle.rs

@@ -1,7 +1,7 @@
 use vstd::prelude::*;
 
-use crate::mm::frame::meta::AnyFrameMeta;
 use crate::mm::frame::meta::mapping::frame_to_index;
+use crate::mm::frame::meta::AnyFrameMeta;
 use crate::mm::frame::Frame;
 use crate::mm::Paddr;
 use crate::specs::mm::frame::frame_specs::*;

ostd/specs/mm/frame/meta_region_owners.rs

@@ -9,7 +9,9 @@ use vstd_extra::cast_ptr::Repr;
 use vstd_extra::ghost_tree::TreePath;
 use vstd_extra::ownership::*;
 
-use super::meta_owners::{MetaPerm, MetaSlotModel, MetaSlotOwner, MetaSlotStorage, REF_COUNT_UNUSED};
+use super::meta_owners::{
+    MetaPerm, MetaSlotModel, MetaSlotOwner, MetaSlotStorage, REF_COUNT_UNUSED,
+};
 use super::*;
 use crate::mm::frame::meta::{
     mapping::{frame_to_index_spec, frame_to_meta, max_meta_slots, meta_addr, META_SLOT_SIZE},

ostd/specs/mm/frame/mod.rs

@@ -6,4 +6,4 @@ pub mod memory_region_specs;
 pub mod meta_owners;
 pub mod meta_region_owners;
 pub mod meta_specs;
-pub mod unique;
+pub mod unique;

ostd/specs/mm/page_table/cursor/cursor_steps.rs

@@ -16,18 +16,14 @@ use crate::specs::mm::Guards;
 use crate::specs::mm::Mapping;
 use crate::specs::mm::MetaRegionOwners;
 
+use crate::mm::page_table::page_size_spec as page_size;
 use crate::specs::mm::frame::mapping::{frame_to_index, meta_to_frame};
 use crate::specs::mm::page_table::cursor::page_size_lemmas::{
-    lemma_page_size_ge_page_size,
-    lemma_page_size_divides,
+    lemma_page_size_divides, lemma_page_size_ge_page_size,
 };
 use vstd_extra::arithmetic::{
-    lemma_nat_align_down_sound,
-    lemma_nat_align_down_within_block,
-    nat_align_down,
-    nat_align_up,
+    lemma_nat_align_down_sound, lemma_nat_align_down_within_block, nat_align_down, nat_align_up,
 };
-use crate::mm::page_table::page_size_spec as page_size;
 
 use core::ops::Range;
 
@@ -382,9 +378,9 @@ impl<'rcu, C: PageTableConfig> CursorOwner<'rcu, C> {
             assert(child_subtree.inv());
             let pto = PageTableOwner(child_subtree);
             assert(pto.view_rec(child_path) =~= child_cont.view_mappings()) by {
-                assert forall |m: Mapping| child_cont.view_mappings().contains(m) implies
+                assert forall |m: Mapping| #[trigger] child_cont.view_mappings().contains(m) implies
                     pto.view_rec(child_path).contains(m) by {
-                    let j = choose |j: int| #![auto]
+                    let j = choose |j: int| #![trigger child_cont.children[j]]
                         0 <= j < child_cont.children.len()
                         && child_cont.children[j] is Some
                         && PageTableOwner(child_cont.children[j].unwrap()).view_rec(
@@ -394,7 +390,7 @@ impl<'rcu, C: PageTableConfig> CursorOwner<'rcu, C> {
                     assert(pto.0.children[j] is Some);
                     assert(pto.0.children[j] == child_cont.children[j]);
                 };
-                assert forall |m: Mapping| pto.view_rec(child_path).contains(m) implies
+                assert forall |m: Mapping| #[trigger] pto.view_rec(child_path).contains(m) implies
                     child_cont.view_mappings().contains(m) by {
                     // view_rec for node: exists i s.t. children[i] is Some && PTO(children[i]).view_rec(...)
                     let j = choose |j: int|
@@ -1182,7 +1178,7 @@ impl<'rcu, C: PageTableConfig> CursorOwner<'rcu, C> {
         };
 
         assert(new_owner.metaregion_sound(regions)) by {
-            assert forall |i: int| #![auto]
+            assert forall |i: int| #![trigger new_owner.continuations[i]]
                 new_owner.level - 1 <= i < NR_LEVELS implies {
                     &&& f(new_owner.continuations[i].entry_own, new_owner.continuations[i].path())
                     &&& new_owner.continuations[i].map_children(f)
@@ -1221,7 +1217,7 @@ impl<'rcu, C: PageTableConfig> CursorOwner<'rcu, C> {
             };
 
             assert(new_owner.metaregion_correct(regions)) by {
-                assert forall |i: int| #![auto]
+                assert forall |i: int| #![trigger new_owner.continuations[i]]
                     new_owner.level - 1 <= i < NR_LEVELS implies {
                         &&& g(new_owner.continuations[i].entry_own, new_owner.continuations[i].path())
                         &&& new_owner.continuations[i].map_children(g)
@@ -1553,7 +1549,7 @@ impl<'rcu, C: PageTableConfig> CursorOwner<'rcu, C> {
         self.cont_entries_metaregion(regions);
 
         assert(new_owner.metaregion_sound(regions)) by {
-            assert forall |i: int| #![auto]
+            assert forall |i: int| #![trigger new_owner.continuations[i]]
                 new_owner.level - 1 <= i < NR_LEVELS implies
                     new_owner.continuations[i].map_children(f)
             by {
@@ -1565,7 +1561,7 @@ impl<'rcu, C: PageTableConfig> CursorOwner<'rcu, C> {
         };
         if self.metaregion_correct(regions) {
             assert(new_owner.metaregion_correct(regions)) by {
-                assert forall |i: int| #![auto]
+                assert forall |i: int| #![trigger new_owner.continuations[i]]
                     new_owner.level - 1 <= i < NR_LEVELS implies
                         new_owner.continuations[i].map_children(g)
                 by {
@@ -1590,8 +1586,8 @@ impl<'rcu, C: PageTableConfig> CursorOwner<'rcu, C> {
             self.level < self.guard_level,
             new_va.inv(),
             new_va.offset == 0,
-            forall |i: int| #![auto] self.level - 1 <= i < NR_LEVELS ==> new_va.index[i] == self.va.index[i],
-            forall |i: int| #![auto] self.guard_level - 1 <= i < NR_LEVELS ==> new_va.index[i] == self.prefix.index[i],
+            forall |i: int| #![trigger new_va.index[i]] self.level - 1 <= i < NR_LEVELS ==> new_va.index[i] == self.va.index[i],
+            forall |i: int| #![trigger new_va.index[i]] self.guard_level - 1 <= i < NR_LEVELS ==> new_va.index[i] == self.prefix.index[i],
         ensures
             self.set_va_spec(new_va).inv(),
     {
@@ -1978,7 +1974,8 @@ impl<'rcu, C: PageTableConfig> CursorOwner<'rcu, C> {
             // With same children and path, view_mappings are the same
             assert forall |m: Mapping| r.view_mappings().contains(m)
                 implies p.view_mappings().contains(m) by {
-                let j = choose |j: int| #![auto]
+                let j = choose |j: int| #![trigger PageTableOwner(r.children[j].unwrap()).view_rec(
+                    r.path().push_tail(j as usize)).contains(m)]
                     0 <= j < r.children.len()
                     && r.children[j] is Some
                     && PageTableOwner(r.children[j].unwrap()).view_rec(
@@ -1989,7 +1986,8 @@ impl<'rcu, C: PageTableConfig> CursorOwner<'rcu, C> {
             };
             assert forall |m: Mapping| p.view_mappings().contains(m)
                 implies r.view_mappings().contains(m) by {
-                let j = choose |j: int| #![auto]
+                let j = choose |j: int| #![trigger PageTableOwner(p.children[j].unwrap()).view_rec(
+                    p.path().push_tail(j as usize)).contains(m)]
                     0 <= j < p.children.len()
                     && p.children[j] is Some
                     && PageTableOwner(p.children[j].unwrap()).view_rec(
@@ -2095,7 +2093,8 @@ impl<'rcu, C: PageTableConfig> CursorOwner<'rcu, C> {
             assert(new_cont.view_mappings() =~= old_cont.view_mappings()) by {
                 assert forall |m: Mapping| old_cont.view_mappings().contains(m)
                     implies new_cont.view_mappings().contains(m) by {
-                    let i = choose |i: int| #![auto]
+                    let i = choose |i: int| #![trigger PageTableOwner(old_cont.children[i].unwrap()).view_rec(
+                        old_cont.path().push_tail(i as usize)).contains(m)]
                         0 <= i < old_cont.children.len()
                         && old_cont.children[i] is Some
                         && PageTableOwner(old_cont.children[i].unwrap()).view_rec(
@@ -2106,7 +2105,8 @@ impl<'rcu, C: PageTableConfig> CursorOwner<'rcu, C> {
                 };
                 assert forall |m: Mapping| new_cont.view_mappings().contains(m)
                     implies old_cont.view_mappings().contains(m) by {
-                    let i = choose |i: int| #![auto]
+                    let i = choose |i: int| #![trigger PageTableOwner(new_cont.children[i].unwrap()).view_rec(
+                        new_cont.path().push_tail(i as usize)).contains(m)]
                         0 <= i < new_cont.children.len()
                         && new_cont.children[i] is Some
                         && PageTableOwner(new_cont.children[i].unwrap()).view_rec(
@@ -2168,7 +2168,3 @@ impl<'rcu, C: PageTableConfig> CursorOwner<'rcu, C> {
 }
 
 }
-
-
-
-

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

@@ -16,16 +16,16 @@ use core::marker::PhantomData;
 use core::ops::Range;
 
 use crate::mm::frame::meta::mapping::frame_to_index;
-use crate::mm::page_table::*;
 use crate::mm::page_prop::PageProperty;
+use crate::mm::page_table::*;
 use crate::mm::{nr_subpage_per_huge, Paddr, PagingConstsTrait, PagingLevel, Vaddr};
 use crate::specs::arch::mm::{MAX_PADDR, MAX_USERSPACE_VADDR, NR_ENTRIES, NR_LEVELS, PAGE_SIZE};
+use crate::specs::arch::PagingConsts;
 use crate::specs::mm::frame::meta_owners::{REF_COUNT_MAX, REF_COUNT_UNUSED};
+use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;
 use crate::specs::mm::page_table::cursor::page_size_lemmas::{
     lemma_page_size_divides, lemma_page_size_ge_page_size, lemma_page_size_spec_level1,
 };
-use crate::specs::arch::paging_consts::PagingConsts;
-use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;
 use crate::specs::mm::page_table::node::GuardPerm;
 use crate::specs::mm::page_table::owners::*;
 use crate::specs::mm::page_table::view::PageTableView;
@@ -171,7 +171,7 @@ impl<'rcu, C: PageTableConfig> CursorContinuation<'rcu, C> {
 
     pub open spec fn map_children(self, f: spec_fn(EntryOwner<C>, TreePath<NR_ENTRIES>) -> bool) -> bool {
         forall |i: int|
-            #![auto]
+            #![trigger self.children[i]]
             0 <= i < self.children.len() ==>
                 self.children[i] is Some ==>
                     self.children[i].unwrap().tree_predicate_map(self.path().push_tail(i as usize), f)
@@ -191,7 +191,7 @@ impl<'rcu, C: PageTableConfig> CursorContinuation<'rcu, C> {
             self.map_children(g),
     {
         assert forall|j: int|
-            #![auto]
+            #![trigger self.children[j]]
             0 <= j < self.children.len()
                 && self.children[j] is Some implies
                 self.children[j].unwrap().tree_predicate_map(
@@ -223,7 +223,7 @@ impl<'rcu, C: PageTableConfig> CursorContinuation<'rcu, C> {
             cont0.map_children(f),
             self.path() == cont0.path(),
             self.children.len() == cont0.children.len(),
-            forall|j: int| #![auto]
+            forall|j: int| #![trigger self.children[j], cont0.children[j]]
                 0 <= j < NR_ENTRIES && j != idx ==>
                 self.children[j] == cont0.children[j],
             self.children[idx] is Some ==>
@@ -233,7 +233,7 @@ impl<'rcu, C: PageTableConfig> CursorContinuation<'rcu, C> {
             self.map_children(g),
     {
         assert forall|j: int|
-            #![auto]
+            #![trigger self.children[j]]
             0 <= j < self.children.len()
                 && self.children[j] is Some implies
                 self.children[j].unwrap().tree_predicate_map(
@@ -276,13 +276,13 @@ impl<'rcu, C: PageTableConfig> CursorContinuation<'rcu, C> {
             self.inv_children()
         ensures
             forall |i:int|
-                #![auto]
+                #![trigger self.children[i]]
                 0 <= i < self.children.len() ==>
                 self.children[i] is Some ==>
                 self.children[i].unwrap().inv()
     {
         let pred = |child: Option<OwnerSubtree<C>>| child is Some ==> child.unwrap().inv();
-        assert forall |i:int| 0 <= i < self.children.len() && self.children[i] is Some implies
+        assert forall |i:int| 0 <= i < self.children.len() && #[trigger] self.children[i] is Some implies
             self.children[i].unwrap().inv()
         by {
             self.inv_children_unroll(i)
@@ -368,7 +368,7 @@ impl<'rcu, C: PageTableConfig> CursorContinuation<'rcu, C> {
     pub open spec fn view_mappings(self) -> Set<Mapping> {
         Set::new(
             |m: Mapping| exists|i:int|
-            #![auto]
+            #![trigger self.children[i]]
             0 <= i < self.children.len() &&
                 self.children[i] is Some &&
                 PageTableOwner(self.children[i].unwrap()).view_rec(self.path().push_tail(i as usize)).contains(m)
@@ -1900,7 +1900,7 @@ impl<'rcu, C: PageTableConfig> CursorOwner<'rcu, C> {
         let g = PageTableOwner::metaregion_sound_pred(regions1);
         let h = PageTableOwner::<C>::path_tracked_pred(regions1);
 
-        assert forall|i: int| #![auto] self.level - 1 <= i < NR_LEVELS implies {
+        assert forall|i: int| #![trigger other.continuations[i]] self.level - 1 <= i < NR_LEVELS implies {
             other.continuations[i].map_children(g)
         } by {
             let cont = self.continuations[i];
@@ -1928,7 +1928,7 @@ impl<'rcu, C: PageTableConfig> CursorOwner<'rcu, C> {
             };
         };
         if self.metaregion_correct(regions0) {
-            assert forall|i: int| #![auto] self.level - 1 <= i < NR_LEVELS implies {
+            assert forall|i: int| #![trigger other.continuations[i]] self.level - 1 <= i < NR_LEVELS implies {
                 other.continuations[i].map_children(h)
             } by {
                 let cont = self.continuations[i];
@@ -2302,8 +2302,8 @@ impl<'rcu, C: PageTableConfig> CursorOwner<'rcu, C> {
 
     pub axiom fn set_va(tracked &mut self, new_va: AbstractVaddr)
         requires
-            forall |i: int| #![auto] old(self).level - 1 <= i < NR_LEVELS ==> new_va.index[i] == old(self).va.index[i],
-            forall |i: int| #![auto] old(self).guard_level - 1 <= i < NR_LEVELS ==> new_va.index[i] == old(self).prefix.index[i],
+            forall |i: int| #![trigger new_va.index[i]] old(self).level - 1 <= i < NR_LEVELS ==> new_va.index[i] == old(self).va.index[i],
+            forall |i: int| #![trigger new_va.index[i]] old(self).guard_level - 1 <= i < NR_LEVELS ==> new_va.index[i] == old(self).prefix.index[i],
         ensures
             *final(self) == old(self).set_va_spec(new_va);
 
@@ -2329,7 +2329,7 @@ impl<'rcu, C: PageTableConfig> CursorOwner<'rcu, C> {
         requires
             old(self).inv(),
             new_va.inv(),
-            forall|i: int| #![auto] old(self).level <= i < NR_LEVELS
+            forall|i: int| #![trigger new_va.index[i]] old(self).level <= i < NR_LEVELS
                 ==> new_va.index[i] == old(self).va.index[i],
             old(self).locked_range().start <= new_va.to_vaddr()
                 < old(self).locked_range().end,
@@ -2475,8 +2475,9 @@ impl<C: PageTableConfig> Inv for CursorView<C> {
     open spec fn inv(self) -> bool {
         &&& self.cur_va < MAX_USERSPACE_VADDR
         &&& self.mappings.finite()
-        &&& forall|m: Mapping| #![auto] self.mappings.contains(m) ==> m.inv()
-        &&& forall|m: Mapping, n: Mapping| #![auto]
+        &&& forall|m: Mapping| #![trigger self.mappings.contains(m)] self.mappings.contains(m) ==> m.inv()
+        &&& forall|m: Mapping, n: Mapping|
+            #![trigger self.mappings.contains(m), self.mappings.contains(n)]
             self.mappings.contains(m) ==>
             self.mappings.contains(n) ==>
             m != n ==>

ostd/specs/mm/page_table/cursor/page_table_cursor_specs.rs

@@ -239,7 +239,7 @@ impl<C: PageTableConfig> CursorView<C> {
         // Mappings fully outside [start, end) are preserved.
         // (A mapping that straddles a boundary may be split, but its sub-mappings
         // outside the range are present — see refinement clause.)
-        &&& forall |m: Mapping| self.mappings.contains(m)
+        &&& forall |m: Mapping| #[trigger] self.mappings.contains(m)
             && (m.va_range.end <= start || m.va_range.start >= end)
             ==> new_view.mappings.contains(m)
         // No mapping in the new view starts inside [start, end), UNLESS it is
@@ -256,9 +256,9 @@ impl<C: PageTableConfig> CursorView<C> {
                 && m.property == parent.property
         // New mappings are either from the old view or are sub-mappings of
         // old entries that straddled a boundary (refinement).
-        &&& forall |m: Mapping| new_view.mappings.contains(m)
+        &&& forall |m: Mapping| #[trigger] new_view.mappings.contains(m)
             ==> self.mappings.contains(m)
-            || exists |parent: Mapping| self.mappings.contains(parent)
+            || exists |parent: Mapping| #[trigger] self.mappings.contains(parent)
                 && parent.va_range.start <= m.va_range.start
                 && m.va_range.end <= parent.va_range.end
                 && m.pa_range.start == (parent.pa_range.start + (m.va_range.start - parent.va_range.start)) as Paddr

ostd/specs/mm/page_table/mod.rs

@@ -511,7 +511,7 @@ impl AbstractVaddr {
             };
             next_va.next_index_preserves_lower_indices(start_level + 1, lower_level);
         } else if next_index == NR_ENTRIES && start_level == NR_LEVELS {
-        } 
+        }
     }
 
     pub proof fn next_index_wrap_condition(self, level: int)
@@ -530,7 +530,7 @@ impl AbstractVaddr {
                 next_va.next_index_wrap_condition(level + 1);
                 self.wrapped_after_carry_equiv(level, level + 1);
                 next_va.next_index_preserves_lower_indices(level + 1, level);
-            } 
+            }
         } else {
             assert(self.index.contains_key(level - 1));
         }

ostd/specs/mm/page_table/owners.rs

@@ -20,10 +20,10 @@ use crate::mm::page_table::{page_size_spec, PageTableEntryTrait, PageTableGuard}
 
 use crate::specs::arch::*;
 use crate::specs::mm::frame::meta_region_owners::MetaRegionOwners;
-use crate::specs::mm::page_table::*;
 use crate::specs::mm::page_table::cursor::page_size_lemmas::{
     lemma_page_size_divides, lemma_page_size_ge_page_size,
 };
+use crate::specs::mm::page_table::*;
 
 use core::ops::Deref;
 

ostd/specs/mm/page_table/view.rs

@@ -58,8 +58,9 @@ impl Mapping {
 /// The physical ranges not overlapping must be maintained by the page table implementation.
 impl PageTableView {
     pub open spec fn inv(self) -> bool {
-        &&& forall|m: Mapping| #![auto] self.mappings has m ==> m.inv()
-        &&& forall|m: Mapping, n:Mapping| #![auto]
+        &&& forall|m: Mapping| #![trigger self.mappings.contains(m)] self.mappings has m ==> m.inv()
+        &&& forall|m: Mapping, n:Mapping|
+            #![trigger self.mappings.contains(m), self.mappings.contains(n)]
             self.mappings has m ==>
             self.mappings has n ==>
             m != n ==> {

ostd/specs/mm/virt_mem_newer.rs

@@ -703,7 +703,7 @@ impl VirtPtr {
                     mem_dst.addr_transl(i) == mem0.addr_transl(i)
                 );
                 assert forall|i: usize|
-                    dst.vaddr <= i < dst.vaddr + n - 1 ==> mem_dst.addr_transl(i) is Some by {
+                    dst.vaddr <= i < dst.vaddr + n - 1 implies mem_dst.addr_transl(i) is Some by {
                     assert(mem_dst.addr_transl(i) == mem0.addr_transl(i));
                 }
             }
@@ -841,7 +841,8 @@ impl GlobalMemView {
 
     pub open spec fn pas_uniquely_mapped(self) -> bool {
         forall|m1: Mapping, m2: Mapping|
-             #[trigger] self.tlb_mappings.contains(m1) && #[trigger] self.tlb_mappings.contains(m2) && m1 != m2 ==>
+             #![trigger self.tlb_mappings.contains(m1), self.tlb_mappings.contains(m2)]
+             self.tlb_mappings.contains(m1) && self.tlb_mappings.contains(m2) && m1 != m2 ==>
             m1.pa_range.end <= m2.pa_range.start || m2.pa_range.end <= m1.pa_range.start
     }