Support building Verus-verified components with ordinary stable Rust

[Chris-Hawblitzel]

So far, we've been using the verus executable to build and compile Verus projects in their entirety. However, there are also scenarios where Verus-verified code is used as a component in a larger unverified Rust-based project. In this case, the Verus-verified component still depends on builtin, builtin_macros, and vstd, which currently depend on special Verus build procedures that include non-stable Rust features.

This pull request observes that once ghost code is erased, builtin, builtin_macros, and vstd don't actually depend on any special Verus build procedures or non-stable Rust features, and can in fact be built with ordinary stable rustc and cargo, making them easier to incorporate as dependencies in larger Rust projects. To take advantage of this, this pull request replaces the verus_macro_erase_ghost cfg flag with two cfg flags, verus_keep_ghost and verus_keep_ghost_body. This supports the two existing scenarios where verus runs rustc with unstable features, plus the new stable-Rust scenario:

• verus_keep_ghost and verus_keep_ghost_body ==> keep all ghost code, as in previous not(verus_macro_erase_ghost)
• verus_keep_ghost and not(verus_keep_ghost_body) ==> keep only ghost stub function declarations, but erase ghost function bodies, as in previous verus_macro_erase_ghost
• not(verus_keep_ghost) and not(verus_keep_ghost_body) ==> erase ghost function bodies and declarations, including declarations in builtin, to enable compiling code with ordinary stable rustc and cargo as part of a larger project

Since not(verus_keep_ghost) and not(verus_keep_ghost_body) are the default configuration, no special cfg flags are required for compiling Verus-verified code with ordinary rustc and cargo. In addition, this pull request adds an ordinary Cargo.toml file for vstd that builds the not(verus_keep_ghost) and not(verus_keep_ghost_body) version of vstd and vstd's dependencies (including builtin, builtin_macros, syn_verus, etc.). Larger Rust projects can easily use this Cargo.toml file to build the dependencies of any Verus-verified code. Finally, this pull request makes building this no-ghost version of vstd part of CI.

Note: this pull request avoids triggering the issue that motivated #709 and is therefore orthogonal to #709 .

[edited to fix misspelling of verus_keep_ghost]

[tjhance]

I was planning to use the unstable allocator_api for #460

Is there a way to keep that?

[Chris-Hawblitzel]

I was planning to use the unstable allocator_api for #460

Is there a way to keep that?

Good question. I guess some projects like Syn are highly configurable based on cfg feature flags. Should we make vstd configurable by a cfg flag so that it can include or exclude code that relies on unstable features? (Or we could overload the verus_keep_ghost cfg flag for this purpose.)

[tjhance]

Well the allocator_api is supposed to be used by executable code. So restricting it to verus_keep_ghost wouldn't help.

[Chris-Hawblitzel]

Well the allocator_api is supposed to be used by executable code. So restricting it to verus_keep_ghost wouldn't help.

Ok, so maybe the proper thing to do is to add a separate cfg flag for executable vstd code that relies on unstable Rust features.

[utaal]

Ok, so maybe the proper thing to do is to add a separate cfg flag for executable vstd code that relies on unstable Rust features.

That makes sense to me if @tjhance believes it would work.

[utaal]

The only concern I have is the potential UB in public verus functions that are safe but have a precondition, which is being discussed here #105 (comment)

But I don't think that has to be resolved before merging, as long as it's clear that we may make breaking changes to the conditionally safe parts of vstd, or to the code produced with ordinary stable Rust, as a result of that discussion.