Revert "prove: RwLockReadGuard::drop"

This reverts commit 799c8ff.

Author: rikosellic

ostd/src/sync/rwlock.rs

@@ -67,19 +67,6 @@ exec const V_MAX_READ_RETRACT_FRACS: u64
     (MAX_READER_MASK + 1) as u64
 }
 
-spec const V_MAX_READ_GUARDS_SPEC: u64 = MAX_READER as u64;
-
-#[verifier::when_used_as_spec(V_MAX_READ_GUARDS_SPEC)]
-exec const V_MAX_READ_GUARDS: u64
-    ensures
-        V_MAX_READ_GUARDS == V_MAX_READ_GUARDS_SPEC,
-        V_MAX_READ_GUARDS == MAX_READER,
-        V_MAX_READ_GUARDS < u64::MAX,
-{
-    assert(MAX_READER < u64::MAX) by (compute_only);
-    MAX_READER as u64
-}
-
 tracked struct RwPerms<T> {
     /// The permission of the `PCell<T>`. 
     /// In the reading state, it can be splited up to `V_MAX_PERM_FRACS:= MAX_READER + 2` pieces,
@@ -97,8 +84,6 @@ tracked struct RwPerms<T> {
     upread_retract_token: UniqueTokenStorage,
     /// Tracks whether there is a live `RwLockUpgradeableGuard`.
     upreader_guard_token: UniqueTokenStorage,
-    /// Tracks the number of live `RwLockReadGuard`s.
-    read_guard_token: TokenStorage<V_MAX_READ_GUARDS>,
 }
 
 ghost struct RwId {
@@ -107,7 +92,6 @@ ghost struct RwId {
     upread_retract_token_id: Loc,
     upreader_guard_token_id: Loc,
     read_retract_token_id: Loc,
-    read_guard_token_id: Loc,
 }
 
 /// The number of `try_read` operations recorded in the lock atomic (created and ongoing) can never reach `2*MAX_READER` to avoid overflow.
@@ -240,7 +224,7 @@ closed spec fn wf(self) -> bool {
         // The number of active `RwLockUpgradeableGuard`, which can only be 0 or 1.
         let active_upgrade_guard: bool = g.upreader_guard_token.is_empty();
         // The number of active `RwLockReadGuard`s.
-        let active_read_guards: int = V_MAX_READ_GUARDS - g.read_guard_token.frac();
+        let active_read_guards: int = total_active_readers - if active_upgrade_guard { 1int } else { 0 };
         // The first `try_upread` that fails, which has not returned yet.
         let pending_failed_upread_attempt: bool = g.upread_retract_token.is_empty();
         // The number of `try_read` attempts that will fail.
@@ -250,8 +234,6 @@ closed spec fn wf(self) -> bool {
         &&& has_upgrade_bit <==> (active_upgrade_guard || pending_failed_upread_attempt)
         // An active `RwLockUpgradeableGuard` cannot coexist with a pending failed `try_upread` attempt.
         &&& !(active_upgrade_guard && pending_failed_upread_attempt)
-        // Active readers are split into plain readers plus at most one upgradeable reader.
-        &&& total_active_readers == active_read_guards + if active_upgrade_guard { 1int } else { 0 }
         // The `READER` bits count the number of all active readers and pending failed `try_read` attempts.
         &&& total_reader_bits + if active_upgrade_guard { 1int } else {0} == total_active_readers +  failed_reader_attempts
         // There is an active `RwLockWriteGuard` iff the `WRITER` bit is set.
@@ -264,7 +246,6 @@ closed spec fn wf(self) -> bool {
         &&& g.cell_perm_resource.wf()
         &&& g.upread_retract_token.wf()
         &&& g.upreader_guard_token.wf()
-        &&& g.read_guard_token.wf()
         &&& g.cell_perm_resource.is_resource_owner() 
         &&& g.cell_perm_resource.has_resource()
         &&& g.cell_perm_resource.is_left() ==> {
@@ -281,7 +262,6 @@ closed spec fn wf(self) -> bool {
         &&& v_id@.upread_retract_token_id == g.upread_retract_token.id()
         &&& v_id@.upreader_guard_token_id == g.upreader_guard_token.id()
         &&& v_id@.read_retract_token_id == g.read_retract_token.id()
-        &&& v_id@.read_guard_token_id == g.read_guard_token.id()
         &&& v_id@.cell_perm_resource_id == g.cell_perm_resource.id()
     }
 }
@@ -336,10 +316,6 @@ impl<T, G> RwLock<T, G> {
         self.v_id@.upreader_guard_token_id
     }
 
-    pub closed spec fn read_guard_token_id(self) -> Loc {
-        self.v_id@.read_guard_token_id
-    }
-
     /// Encapsulates the invariant described in the *Invariant* section of [`RwLock`].
     #[verifier::type_invariant]
     pub closed spec fn type_inv(self) -> bool {
@@ -363,22 +339,19 @@ impl<T, G> RwLock<T, G> {
             let tracked read_retract_token = TokenStorage::<V_MAX_READ_RETRACT_FRACS>::alloc(());
             let tracked upread_retract_token = UniqueTokenStorage::alloc(());
             let tracked upreader_guard_token = UniqueTokenStorage::alloc(());
-            let tracked read_guard_token = TokenStorage::<V_MAX_READ_GUARDS>::alloc(());
         }
         let ghost v_id = RwId {
             frac_id,
             cell_perm_resource_id: cell_perm_resource.id(),
             upread_retract_token_id: upread_retract_token.id(),
             upreader_guard_token_id: upreader_guard_token.id(),
             read_retract_token_id: read_retract_token.id(),
-            read_guard_token_id: read_guard_token.id(),
         };
         let tracked perms = RwPerms {
             cell_perm_resource,
             read_retract_token,
             upread_retract_token,
             upreader_guard_token,
-            read_guard_token,
         };
 
         Self {
@@ -458,7 +431,6 @@ impl<T  /*: ?Sized*/ , G: SpinGuardian> RwLock<T, G> {
             let tracked mut perm: Option<RwFrac<T>> = None;
             let tracked mut retract_read_token: Option<Token<V_MAX_READ_RETRACT_FRACS>> = None;
             let tracked mut left_token = None;
-            let tracked mut read_guard_token: Option<Token<V_MAX_READ_GUARDS>> = None;
         }
         proof!{
             use_type_invariant(self);
@@ -482,7 +454,6 @@ impl<T  /*: ?Sized*/ , G: SpinGuardian> RwLock<T, G> {
                     perm = Some(tmp.split(1int));
                     g.cell_perm_resource.put_resource_left(tmp);
                     left_token = Some(g.cell_perm_resource.split_left_without_resource(1int));
-                    read_guard_token = Some(g.read_guard_token.split_one());
                 } else {
                     retract_read_token = Some(g.read_retract_token.split_one());
                 }
@@ -494,7 +465,6 @@ impl<T  /*: ?Sized*/ , G: SpinGuardian> RwLock<T, G> {
                 guard,
                 v_perm: Tracked(perm.tracked_unwrap()),
                 v_cell_token: Tracked(left_token.tracked_unwrap()),
-                v_read_token: Tracked(read_guard_token.tracked_unwrap()),
             })
         } else {
             // self.lock.fetch_sub(READER, Release);
@@ -677,7 +647,6 @@ pub struct RwLockReadGuard<'a, T /*: ?Sized*/, G: SpinGuardian> {
     inner: &'a RwLock<T, G>,
     v_perm: Tracked<RwFrac<T>>,
     v_cell_token: Tracked<Left<RwFrac<T>,NoPerm<T>,V_MAX_PERM_FRACS>>,
-    v_read_token: Tracked<Token<V_MAX_READ_GUARDS>>,
 }
 
 /*
@@ -696,10 +665,8 @@ impl<'a, T, G: SpinGuardian> RwLockReadGuard<'a, T, G> {
         &&& self.inner.cell_perm_resource_id() == self.v_cell_token@.id()
         &&& self.inner.frac_id() == self.v_perm@.id()
         &&& self.inner.cell_id() == self.v_perm@.resource().id()
-        &&& self.inner.read_guard_token_id() == self.v_read_token@.id()
         &&& self.v_perm@.frac() == 1
         &&& self.v_cell_token@.frac() == 1
-        &&& self.v_read_token@.frac() == 1
         &&& !self.v_cell_token@.is_resource_owner()
     }
 }
@@ -749,18 +716,16 @@ impl<T /*: ?Sized*/, G: SpinGuardian> RwLockReadGuard<'_, T, G>
         }
         let Tracked(perm) = self.v_perm;
         let Tracked(token) = self.v_cell_token;
-        let Tracked(read_token) = self.v_read_token;
         // self.inner.lock.fetch_sub(READER, Release);
         atomic_with_ghost!(
             self.inner.lock => fetch_sub(READER);
             update prev -> next;
             ghost g => {
-                let prev_usize = #[verifier::truncate] (prev as usize);
-                let next_usize = #[verifier::truncate] (next as usize);
+                let prev_usize = prev as usize;
+                let next_usize = next as usize;
                 lemma_consts_properties_value(prev_usize);
                 lemma_consts_properties_value(next_usize);
                 lemma_consts_properties_prev_next(prev_usize, next_usize);
-                g.read_guard_token.combine(read_token);
                 g.cell_perm_resource.validate_with_left(&token);
                 g.cell_perm_resource.join_left(token);
                 let tracked mut rem = g.cell_perm_resource.take_resource_left();