Replace Some_0 with 0

.vscode/settings.json

@@ -39,4 +39,12 @@
         "miri",
         "verus_keep_ghost"
     ],
+    "verus-analyzer.check.overrideCommand": [
+        "cargo",
+        "dv",
+        "verify",
+        "--targets",
+        "ostd",
+    ],
+    "verus-analyzer.checkOnSave": false,
 }

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

@@ -46,8 +46,8 @@ impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> Repr<MetaSlotStorage> for Link<M> {
                 &&& M::wf(link.slot, perm.storage)
                 &&& (link.next is Some) == (perm.next_ptr is Some)
                 &&& (link.prev is Some) == (perm.prev_ptr is Some)
-                &&& link.next is Some ==> link.next->Some_0 == perm.next_ptr->Some_0.addr()
-                &&& link.prev is Some ==> link.prev->Some_0 == perm.prev_ptr->Some_0.addr()
+                &&& link.next is Some ==> link.next->0 == perm.next_ptr->0.addr()
+                &&& link.prev is Some ==> link.prev->0 == perm.prev_ptr->0.addr()
             },
             _ => false,
         }

ostd/specs/mm/virt_mem_newer.rs

@@ -117,15 +117,15 @@ impl MemView {
     ///
     /// Equivalent to resolving via [`Self::addr_transl`] and reading from [`Self::memory`].
     pub open spec fn read(self, va: usize) -> raw_ptr::MemContents<u8> {
-        let (pa, off) = self.addr_transl(va)->Some_0;
+        let (pa, off) = self.addr_transl(va)->0;
         self.memory[pa].contents[off as int]
     }
 
     /// Specification write through virtual translation.
     ///
     /// Returns a new [`MemView`] with one byte updated, preserving all mappings.
     pub open spec fn write(self, va: usize, x: u8) -> Self {
-        let (pa, off) = self.addr_transl(va)->Some_0;
+        let (pa, off) = self.addr_transl(va)->0;
         MemView {
             memory: self.memory.insert(pa, FrameContents {
                 contents: self.memory[pa].contents.update(off as int, raw_ptr::MemContents::Init(x)),
@@ -137,8 +137,8 @@ impl MemView {
 
     /// Whether two virtual addresses denote equal byte contents in this view.
     pub open spec fn eq_at(self, va1: usize, va2: usize) -> bool {
-        let (pa1, off1) = self.addr_transl(va1)->Some_0;
-        let (pa2, off2) = self.addr_transl(va2)->Some_0;
+        let (pa1, off1) = self.addr_transl(va1)->0;
+        let (pa2, off2) = self.addr_transl(va2)->0;
         self.memory[pa1].contents[off1 as int] == self.memory[pa2].contents[off2 as int]
     }
 

ostd/src/sync/mutex.rs

@@ -34,7 +34,7 @@ closed spec fn wf(self) -> bool {
     invariant on lock with (val) is (v: bool, g: Option<PointsTo<T>>) {
         let active_guard = g is None;
         &&& v <==> active_guard
-        &&& g is Some ==> g->Some_0.id() == val.id()
+        &&& g is Some ==> g->0.id() == val.id()
     }
 }
 }
@@ -118,7 +118,7 @@ impl<T  /* : ?Sized */ > Mutex<T> {
         with
             -> locked_state: Tracked<Option<PointsTo<T>>>,
         ensures
-            ret ==> locked_state@ is Some && locked_state@->Some_0.id() == self.cell_id(),
+            ret ==> locked_state@ is Some && locked_state@->0.id() == self.cell_id(),
             !ret ==> locked_state@ is None,
     )]
     fn acquire_lock(&self) -> bool {

ostd/src/sync/once.rs

@@ -86,7 +86,7 @@ pub closed spec fn wf(&self) -> bool {
                 &&& v == INITED
                 &&& points_to.id() == cell.id()
                 &&& points_to.value() is Some
-                &&& f@.inv(points_to.value()->Some_0)
+                &&& f@.inv(points_to.value()->0)
             }
         }
     }

ostd/src/sync/rwlock.rs

@@ -254,12 +254,12 @@ closed spec fn wf(self) -> bool {
         &&& g.read_retract_token.id() == v_id@.read_retract_token_id
         &&& g.upread_retract_token is Some ==>
             {
-                let token = g.upread_retract_token->Some_0;
+                let token = g.upread_retract_token->0;
                 &&& token.wf()
                 &&& token.id() == v_id@.upread_retract_token_id
             }
         &&& g.upreader_guard_token is Some ==> {
-            let token = g.upreader_guard_token->Some_0;
+            let token = g.upreader_guard_token->0;
             wf_upgradeable_guard_token(v_id@.core_token_id, v_id@.frac_id, val.id(), token)
         }
         &&& match g.read_guard_token {

ostd/src/sync/rwmutex.rs

@@ -197,12 +197,12 @@ closed spec fn wf(self) -> bool {
         &&& g.read_retract_token.wf()
         &&& g.read_retract_token.id() == v_id@.read_retract_token_id
         &&& g.upread_retract_token is Some ==> {
-            let token = g.upread_retract_token->Some_0;
+            let token = g.upread_retract_token->0;
             &&& token.wf()
             &&& token.id() == v_id@.upread_retract_token_id
         }
         &&& g.upreader_guard_token is Some ==> {
-            let token = g.upreader_guard_token->Some_0;
+            let token = g.upreader_guard_token->0;
             wf_upgradeable_guard_token(v_id@.core_token_id, v_id@.frac_id, val.id(), token)
         }
         &&& match g.read_guard_token {

vstd_extra/src/external/nonzero.rs

@@ -141,7 +141,7 @@ impl OrdSpecImpl for NonZeroUsize {
     }
 
     open spec fn cmp_spec(&self, other: &Self) -> Ordering {
-        vstd::std_specs::cmp::PartialOrdSpec::partial_cmp_spec(self, other)->Some_0
+        vstd::std_specs::cmp::PartialOrdSpec::partial_cmp_spec(self, other)->0
     }
 }