Handle trailing newlines for broadcast uses

[jaybosamiya]

Adds an extra trailing newline for broadcast use groups, exemplified by this diff:

Essentially, this PR handles the situation brought up by @utaal-b in #53. To lead to good output, this required handling a few special cases:

• presence of multiple broadcast use items in the same fn
• comments between those items
• top-level broadcast use items

I've handled each of these cases to produce good output. Additionally, the snapshot test in this is is an expanded version of what @utaal-b proposed in #53.

---

NOTE: This PR causes an update to the vstd snapshot. This is intentional (due to style change), but will require coordination on https://github.com/verus-lang/verus when the new version of verusfmt is released. This should not block merging this PR, but yeah, from a release standpoint, will need some coordination to prevent CI failures. I'll open a PR there soon (EDIT: verus-lang/verus#1062)

[parno]

Looks reasonable to me. Should we apply this to other items (e.g., global)?

[jaybosamiya]

Good question. With this PR as a blueprint, adding such code to other similar things should be fairly straightforward, but I think we should refrain from adding for such situations until we see actual code that would benefit from the additional newlines.

[utaal]

Thank you for working on this. One concern: I don't think rustfmt makes changes to add/remove empty lines in a block (as those tend to be introduced as a way to logically group/separate chunks of code by the developer), I'm a bit uneasy about departing from that general principle.

[jaybosamiya]

Given verusfmt's design, we haven't found a clean enough way to maintain empty lines in blocks (even before this broadcast use case, that this PR impacts); we have attempted to come up with approaches to remedy this in the past, but none were satisfactory enough. In short, if we want to handle the double-newline, we'd either need to do a lot more tracking of whitespace in the parser (making the verus.pest unreadable and hard to update correctly), or do a lot more tracking of spans in the printer, and have special casing (making lib.rs much harder to deal with).

I can see pros and cons with rustfmt's principle regarding this; and personally I do think we should preserve empty lines in a block; however, until we find a good way to handle this (PRs welcome!), the current approach of opinionated decisions on separations is the best we've got.

Fwiw, as a workaround for logically separate chunks, an empty comment line (just a // on its own) works for when a user wants to keep things separated, but verusfmt wants to combine those blocks together. This is not ideal, of course, but with the current design, that's as close as we get.

[utaal]

Ah! I suspected this might be the case but didn't know about the attempts you've already made. Thanks for the write-up on the challenges and trade-off.

This choice makes sense to me, then. Thanks!