[cargo-verus] bug: empty `VerusItems` in workspace

[CleveGreen]

I just came across a rather weird ICE with cargo-verus / rust_verify, I call it weird as it wasn't due to me doing anything weird this time. This issue is easy to reproduce, if you create a library in a workspace that never uses anything from vstd and run cargo verus verify it will panic. I'm not exactly sure why this requires a workspace, but I tried it outside of a workspace and the issue went away.

In this scenario, rust_verify::verus_items::from_diagnostic_items will return an empty VerusItems struct, which then leads to the invocation of rust_verify::erase::setup_verus_ctxt_for_thir_erasure (in rust_verify::verifier at line 2954) to panic when trying to get the erased_ghost_value_fn_def_id.

Here's a simple workspace to use for reproducing this error, it is fairly straightforward to set up if uncomfortable with random tars: verus-workspace-ice.tar.gz

This isn't a major issue, but I am in quite a large workspace with verus and the library not yet referencing vstd anywhere wasn't what I expected the issue to be... so it took me on a bit of a wild goose chase.

[parno]

Sorry to hear you ran into that oddity. cargo verus is still a bit experimental at this point, and I don't think anyone has tried it at any scale in a workspace, so there are likely to be some lingering issues there. We're working to improve the cargo verus experience, however, so hopefully things will get smoothed out in the next few months.