Evaluate using more advanced compiler optimizations like LTO and PGO

[zamazan4ik]

Hi! Thank you a lot for the project.

I have several suggestions/ideas that you possibly could find useful for the project:

• Enable Link-Time Optimization (LTO) for Verus. It can help with reducing the binary size significantly and allows to a compiler perform optimizations more efficiently so performance improvements also are expected from enabling LTO. If you think that for a regular Release build profile LTO affects build times too much, I can suggest just creating a dedicated release-lto build profile.
• Try to apply Profile-Guided Optimization (PGO). I tested PGO on many applications in different software domains - all the results are available at https://github.com/zamazan4ik/awesome-pgo . I think it could be interesting to test PGO with Verus. For Rust projects, I suggest starting with PGO via the cargo-pgo tool. If you already have such benchmarks - could you please share the performance numbers for that?
• After PGO I can recommend taking a look at Post-Link Optimization (PLO) and tools like LLVM BOLT. However, it makes sense to do it only after applying PGO since PGO is a much more stable optimization technique compared to PLO.

I would be happy to answer all your questions about LTO, PGO and PLO. Thank you.