Refactor Rwlock with new token libraries (#355)

* Rename FracGhostStorage into FracGhostResource

* Improve Frac library

* Update rwlock

* Begin refactor

* Refactor Inv

* Add `arbitrary` in `FracResource`

* Add `tracked_swap` in `Sum`

* Minor

* Fix operator precedence error

* Try to prove try_write

* prove: sync::rwlock::try_write

* Update sum token library

* Write and try_write

* fmt vstd_extra

* read and try_read

* upread and try_upread

* Prove deref

* Upgrade and try_upgrade

* Try to prove Drop

* Loose a constraint in FracResource

* Try to modify the library

* prove: sync::rwlock::try_read

* prove: RwLockWriteGuard::drop

* prove RwLock::new

* fmt

* fix: syntax error caused by format

* chore: enable rwarc

* Minor simplification

---------

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

Author: rikosellic