Erase ghost code by default

[hayley-leblanc]

This PR makes the verus! macro's default behavior be to erase ghost code and requires a new configuration flag, verus_macro_keep_ghost, when ghost code should be kept for verification. verus_macro_keep_ghost replaces usage of the old flag verus_macro_erase_ghost.

With this PR, it is now possible to use cargo run or cargo build without any additional flags on a crate that uses the verus! macro to build or run an executable. There are some limitations and TODOs before this will work with anything beyond extremely basic Verus code -- most notably, since vstd is not a crate that can be used as a dependency, the crate being built can't use anything from vstd. I plan to look into this next.

I also plan to write up some documentation about how to use cargo to build/run Verus code; for now, the main things to know are:

1. builtin_macros must be included as a dependency in the target crate's Cargo.toml file.
2. Any imports that are only used for ghost code/by Verus and are not linked in as dependencies (e.g., builtin) should be marked with #[cfg(verus_macro_keep_ghost)].

[hayley-leblanc]

This PR now lets Verus code be run with rustc/cargo with no changes to source code at all and adds a Cargo.toml file to pervasive/ so that vstd can be built as a crate. The crate containing verified code should include builtin_macros, builtin, and vstd as local dependencies.

This PR depends on #709, so it will stay a draft at least until that is merged.

[hayley-leblanc]

Closing as these changes are subsumed by #733.