Allow marking a file as skipped

[jaybosamiya]

Currently, a file needs to be parse-able to be able to add a #[verusfmt::skip] declaration to an item. However, it should be possible to support a file-level #![verusfmt::skip] declaration that doesn't need any parser support (at least nothing any further than src/verus-minimal.pest).

This can help unblock new syntax or features in Verus that are being blocked by yet-to-be-added support in verusfmt. However, I am concerned that this might lead to files being accidentally left as unformatted for too long. One mitigation for this is to attempt a parsing check anyways if #![verusfmt::skip] is found, and if parsing succeeds, then throw in a warning saying that more specific #[verusfmt::skip]s are preferred. If we're being fancy, we can even suggest locations to insert those in based on the results of --check, but I think at minimum, an implementation of this should do a "warn if parsing succeeds" check.

---

CC: @Chris-Hawblitzel who asked if there was a way to skip an entire file