toolchain: set x86 as verification target and use no_std accross the project

[rikosellic]

After careful investigation of SMT files on different platforms, we find that the regression in macOS and aarch-linux verification performance is PARTLY caused by a mix of the platform on which Verus is running and the platform on which the verified Asterias version is supposed to run! Therefore, anyone using Verus on an ARM architecture machine (typically macOS with Apple silicon) previously would ignore any Verus code under [cfg(target_arch)].

This PR hardcodes x86_64 as the target Asterinas version to be verified. Consequently, disable any std usage in vstd, vstd_extra and ostd.

[hiroki-chen]

I tested around the generated SMT2 files and used different Z3 backends and all had different behaviors. I'm trying different Z3 versions now.

[hiroki-chen]

The immediate remedy is to decompose the large proof function of lemma_frame_drop_pre_derivable into smaller pieces as we suspect that Z3 will instantiate quantifiers differently on different architecture and the internal algorithm might be flaky.

[Marsman1996]

The doc building error will be fixed with asterinas/rust-deductive-verifier#37