Add verus tool setup scripts + CI + dependencies + import some proofs from verismo

Signed-off-by: Ziqiao Zhou <[email protected]>

Verify more in address mod & Split verismo to verify_proof and verify_external.

* Verify more in address mod.
* Rename spec and improve the definition of canonical address
* Most functions for VirtAddr are verified.
* Move broadcast proofs into address_inner.verus.rs
* Split verismo lib into verify_proof and verify_external.
* Improve verification.md
* Add verify_external to define spec for externals
* No dep verify by default
* Fix CI
* Revert changes in existing ci
* change name in verify.yml
* Use verus main branch
* Upgrade verus lib to latest main branch

Signed-off-by: ziqiao zhou <[email protected]>

---------

Signed-off-by: ziqiao zhou <[email protected]>
Signed-off-by: Ziqiao Zhou <[email protected]>

Simplify the seq_macros
Refine the specification for Option::map

Signed-off-by: Ziqiao Zhou <[email protected]>

* Upgrade verus to support v1.82.

* Cleanup build.rs
* Set verus lib and tool to the rev supporting v1.82

Signed-off-by: Ziqiao Zhou <[email protected]>

* Move vstd.verus.rs to verus vstd & mark memory-related as external

* memory related verification needs to add a memory permission and will
  do it later

Signed-off-by: Ziqiao Zhou <[email protected]>

* Revert unnecessary change after verus upgrade

* revert rust version
* revert some code due to version change

Signed-off-by: Ziqiao Zhou <[email protected]>

* fmt

---------

Signed-off-by: Ziqiao Zhou <[email protected]>

Add example & links about verus

Signed-off-by: Ziqiao Zhou <[email protected]>

Do not run CI for verification.

Signed-off-by: Ziqiao Zhou <[email protected]>

* Upgrade verus to avoid warn in global size
* Install verusfmt via cargo install

Signed-off-by: Ziqiao Zhou <[email protected]>

* Remove vpath.sh since it is only used in verify.yml CI

Signed-off-by: Ziqiao Zhou <[email protected]>