RwLock (#303)

* Add empty RwLock invariant

* spec: add `wf` in  rwlock

* Merge fix

* Try to prove new

* Prove `RwLock::new`

* Add invariant for RwLockReadGuard

* Minor

* Fix invariant

* Rewrite `RwLock::get_mut` and `as_ptr`

* add commented original code

* verifiable: make code compilable for Verus

* fix

* format

* Add try_write proof skeleton

* prove: admit in `RwLock::try_write`

* Simplify try_wrtite proof

* prove: `try_write_arc`

* prove: `try_upread`

NOTE: this modify the spec code

* Revert "prove: `try_upread`"

This reverts commit 99bd09f.

* Add a permission field in UpgradeableGuard

* prove: `RwLock::try_upread`

WARNING: exec code modified

* Revert "prove: `RwLock::try_upread`"

This reverts commit 93d2636.

* Some progress in try_upread

* Refine Inv

* rename

* Prove admit in try_upread

* Prove some admit in try_upread

* Prove try_upread

* prove: try_upread_arc

* chore: remove external_body for upper API

* refine the inv

* Refine the inv and add some doc

* Add bit lemma useful in proving try_read

* Add a helper function

* Add try_read proof skeleton

* Inv overhaul

* proof progress

* prove: 1 admit in `try_read`

* prove: try_read

* Simplify proof

* Minor

* fmt

* prove: try_read_arc

* Minor doc update

* verifiable: all functions in rwlock

* verifiable: rwlock.rs

* doc: enable doc for rwlock

* Simplify proof

* prove: `try_upgrade` and `upgrade`

* verifiable: add original code as the comment

* Remove legacy `downgrade`

* Migrate to latest RwLock

* Deprecate deref_spec

* prove: RwLock::new again

* Prove deref and simplify

* Simplify proof

---------

Co-authored-by: Marsman1996 <lqliuyuwei@outlook.com>

Author: rikosellic

ostd/src/sync/mod.rs

@@ -16,11 +16,8 @@ pub use self::{
     },
     //mutex::{ArcMutexGuard, Mutex, MutexGuard},
     rcu::{non_null /*, Rcu, RcuDrop, RcuOption, RcuOptionReadGuard, RcuReadGuard*/},
-    /*rwarc::{RoArc, RwArc},
-    rwlock::{
-        ArcRwLockReadGuard, ArcRwLockUpgradeableGuard, ArcRwLockWriteGuard, RwLock,
-        RwLockReadGuard, RwLockUpgradeableGuard, RwLockWriteGuard,
-    },
+    /*rwarc::{RoArc, RwArc},*/
+    rwlock::{RwLock, RwLockReadGuard, RwLockUpgradeableGuard, RwLockWriteGuard},/*
     rwmutex::{
         ArcRwMutexReadGuard, ArcRwMutexUpgradeableGuard, ArcRwMutexWriteGuard, RwMutex,
         RwMutexReadGuard, RwMutexUpgradeableGuard, RwMutexWriteGuard,