Track: add `vostd` to `verita`

[hiroki-chen]

The verification for ostd is about to complete; at least we've almost finished mm and sync so far. To promote community awareness of our ongoing verification efforts, it's helpful to include our project to verita, a crater-inspired benchmarking tool for exploring verus verification usages of different projects.

There are many mid-to-large projects available in the verita registry:

• Anvil (OSDI'24): practical, formally verified, cluster management controllers.
• SVSM (part of the CCC open-source project, part of the Linux foundation): A CVM monitor (partially verified)
• Verified storage (OSDI'25): Storage systems with verified correctness properties

I have tested verita on our repo and it worked really fine. The cargo verus focus command avoids the pain of rebuilding verifying dependencies across different crates so that we can separately verify the targets we want in the configuration. There are some minor issues though.

IMO we can wait for a "stable" version of vostd and create a PR to include the project to official verus repo.

[hiroki-chen]

@rikosellic, @Marsman1996 Suggestions and comments are welcomed!

[rikosellic]

This cargo verus focus command is really interesting. Does it just completely avoid building any other dependencies, or will it rebuild the dependencies if they are out of date, like cargo dv verify does?

[hiroki-chen]

This cargo verus focus command is really interesting. Does it just completely avoid building any other dependencies, or will it rebuild the dependencies if they are out of date, like cargo dv verify does?

All packages reachable from the top-level selection are still processed with verus, but deps are treated with the --no-verify option. In other words, non-focused dependencies are built but not verified.