Simplifying installation and use of Verus

[parno]

Here's a proposal that @Chris-Hawblitzel, @jaybosamiya-ms, and I discussed this afternoon. It's relevant to #1758.

To simplify installing and using Verus in production settings, here's a future we'd like to reach. It assumes that in the future, nearly everyone will be using cargo verus, rather than invoking verus directly, just like most Rust developers use cargo build, not rustc.

The plan centers on cargo-verus, which will be hosted on crates.io and hence installable via cargo install cargo-verus, or it can be installed via a rustup-style curl ... | sh command that we provide on the Verus site.

We will extend cargo-verus with the functionality needed to acquire all of the functionality needed to run Verus. This includes:

1. rustc -- We'll instrument cargo-verus to confirm (via rustup) that the Verus-required Rust toolchain is installed (and if it's not, use rustup to install it). In the unlikely event (b/c the user is already running cargo-verus with cargo) that rustup is missing, cargo-verus will politely suggest installing it.
2. z3 -- We'll instrument cargo-verus to fetch the correct version of Z3 from Z3's GitHub release page and install it in a local cache (XDG).
3. vstd -- This will be hosted on crates.io. We'll want to ensure the crates can be built without Verus, i.e., by normal Rust compilation. From a quick scan, this seems largely feasible.
4. verus binary -- For now, the plan is for cargo-verus to fetch a release from the Verus GitHub releases. In the long run, it might be desirable to host verus on crates.io as well. This might be feasible if we could move functionality that is currently in vargo into a build.rs file instead.

Versioning

The current proposal is that cargo-verus will be shipped with baked-in expected versions for each of the components above. Those are the versions it will expect to find in its cache and that it will fetch if it fails to find them. The current proposal is that every time a cargo verus command is run, it will start by checking for expected versions and fetching any that are missing. Hence, there is no need for an explicit cargo verus install command.

End users can move to the next working version set by running cargo verus update, which would fetch the latest version of cargo-verus, which may have new version expectations for one or more of the components above. End users who like their current state, can avoid unexpected component updates by sticking with a particular version of cargo-verus.

We could also support allowing end users to override these versions through environment variables, the way we currently do for Z3.

Crates using Verus for verfication purposes would continue to add vstd and company to the [dependencies] section of their Cargo.toml file. Since vstd et al. would be hosted on crates.io, users could specify version numbers instead of GitHub commits. If the developer published one of these crates, other non-Verus users could consume them by having cargo pull the necessary vstd dependencies from crates.io, just like any other dependency.

If cargo-verus runs on a crate that specifies in its Cargo.toml a version of vstd that differs from what cargo-verus expects, we will treat this as an error and suggest that the user either (a) update their Cargo.toml file, or (b) invoke a command-line flag to override the error.

Deployment

We can reach the future above by following a rough plan of:

1. Ensure vstd et al. can build without Verus and push them to crates.io. Add this step to the CI that publishes Verus releases.
2. Update cargo-verus with functionality to find/install the components above. Once this is robust, make it the default behavior for cargo verus commands.
3. Host cargo-verus on crates.io, and add pushing updates of cargo-verus to the CI release action.
4. Update cargo-verus with an update command for grabbing and installing the latest version of itself.

[jaybosamiya]

Useful crates for building this out:

• https://lib.rs/crates/dirs (for the local cache, specifically, see https://docs.rs/dirs/latest/dirs/fn.cache_dir.html; we probably want to store to {cache_dir}/verus/{versionhash}/files, where versionhash is a hash of the Verus version; https://docs.rs/dirs/latest/dirs/fn.cache_dir.html can store a TOML file that contains vstd->verus and verus->vstd version lookups)
• https://lib.rs/crates/reqwest (to actually download things)
• https://lib.rs/crates/axoupdater (for an eventual cargo verus self-update)
• https://lib.rs/crates/tempfile (if needed)
• https://lib.rs/crates/toml (or https://lib.rs/crates/toml_edit if we want to (eventually) support a nicer cargo verus update vstd or similar)
• https://lib.rs/crates/semver (if we want more precise errors/warns for some cases; I don't think we are doing full semver right now though, so probably not needed right now)

[parno]

Summarizing some discussion points from today's Verus meeting:

1. There's a desire to be able to override where cargo-verus fetches the Verus binary, rustc, and Z3 from, since some custom build environments don't want to allow fetching from external Internet locations. We could support this via environment variables. Another possibility is that such build environments can pre-populate the cache with the desired versions, so that cargo-verus finds them in place when it goes looking, and hence does not need to make use of Internet connectivity.
2. Rather than embedding version numbers into cargo-verus, cargo-verus could instead maintain/retrieve/construct a list of valid version combinations for vstd and verus. Then, based on the version of vstd specified in a particular crate's Cargo.toml file, it can find and install an appropriate version of the verus binary. That way, developers can work on multiple Verus projects that might be using different versions of vstd.
3. We should rename builtin to verus_builtin and builtin_macros to verus_builtin_macros for polite usage of the crates.io namespace. We can make vstd depend on both of these (renamed) crates, and have it re-export the verus! macro from verus_builtin_macros. That way, end users only need to put vstd into their [dependencies] list, and cargo will do the right thing. We could potentially extend cargo-verus to detect when the Cargo.toml file already has entries for all three crates and suggest that developers simplify down to just vstd.

[parno]

It looks like builtin_macros depends on our forked versions of syn and pretty_please, so I think we'll need to publish them to crates.io as well. Also, vstd depends on state_machine_macros, so I'll rename that to verus_state_machine_macros, and we'll need to publish that too.