Make non-verus-macro items external by default

[Chris-Hawblitzel]

When --external-by-default is passed on the command line, treat items outside the verus! macro as #[verifier::external] unless marked #[verifier::verify]. This makes it easier to verify small amounts of code inside a larger unverified Rust crate. I would expect uses of #[verifier::verify] to be rare for now; it would be more common to wrap the verified code inside verus!.

[tjhance]

Could we make it a crate setting (or even, a module setting) instead of a command line flag? e.g., with a crate attribute

#![verifier::verify_all]

I feel like that would be more appropriate for multi-crate projects where you might be combining verified and unverified crates.

[utaal]

I would also prefer making it a crate-level attribute, rather than a command line flag. This is also because I'd like to avoid having too many flags that significantly change the behavior of the tool (and that one needs to remember to include in the command line when working with a specific project). In fact, I think this is an argument for making --arch-word-bits a crate-level flag too (which need not be part of this PR, obviously).

[Chris-Hawblitzel]

I updated the PR to make external-by-default the default behavior, with a --no-external-by-default option for backwards compatibility to get the old behavior. In the long run, I wouldn't expect people to use --no-external-by-default, although it may be used internally in our tests.